add manual trivial application to conseq variant (#848)

Author: oskgo

src/phl/ecPhlConseq.ml

@@ -1129,7 +1129,7 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
                   t_intros_i [m;h0] @! t_cutdef
                     (ptlocal ~args:[pamemory m; palocal h0] hi)
                     mpre @! EcLowGoal.t_trivial;
-                  t_mytrivial;
+                  t_mytrivial @! t_intros_i [m; h0] @! t_apply_hyp h0;
                   t_apply_hyp hh];
                 tac pre posta @+ [
                   t_apply_hyp hi;

tests/conseq_phoare_hoare.ec

@@ -0,0 +1,14 @@
+require import Real.
+
+module Foo = {proc foo() = {}}.
+
+lemma foo_ll : islossless Foo.foo by islossless.
+
+op [opaque] p = predT<:int>.
+
+lemma foo_h: hoare [ Foo.foo : true ==> forall j, p j]. 
+proof. by proc; auto => /> j; rewrite /p. qed.
+
+lemma foo_p: phoare[ Foo.foo : true ==> forall j, p j] = 1%r.
+by conseq foo_ll foo_h.
+qed.