From b667d1b49bef5c3804172f63391c9f01f57eae03 Mon Sep 17 00:00:00 2001
From: Oskar Goldhahn <oskar.goldhahn@ntnu.no>
Date: Tue, 9 Dec 2025 13:50:17 +0100
Subject: [PATCH] add manual trivial application to conseq variant

---
 src/phl/ecPhlConseq.ml       |  2 +-
 tests/conseq_phoare_hoare.ec | 14 ++++++++++++++
 2 files changed, 15 insertions(+), 1 deletion(-)
 create mode 100644 tests/conseq_phoare_hoare.ec

diff --git a/src/phl/ecPhlConseq.ml b/src/phl/ecPhlConseq.ml
index 90a07c86f..faedc54a7 100644
--- a/src/phl/ecPhlConseq.ml
+++ b/src/phl/ecPhlConseq.ml
@@ -1120,7 +1120,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;
diff --git a/tests/conseq_phoare_hoare.ec b/tests/conseq_phoare_hoare.ec
new file mode 100644
index 000000000..021622544
--- /dev/null
+++ b/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.