trivial needs some handholding

Author: Cameron-Low

src/phl/ecPhlCond.ml

@@ -150,7 +150,6 @@ end = struct
         let+ tc = EcPhlSkip.t_skip tc in
         let+ tc = EcLowGoal.t_intro_s `Fresh tc in
         let+ tc = EcLowGoal.t_elim_and tc in
-
         let e = EcEnv.LDecl.fresh_id (FApi.tc1_hyps tc) "e" in
 
         let+ tc = EcLowGoal.t_intros_i [e] tc in
@@ -173,10 +172,26 @@ end = struct
       in
 
       let clean (tc : tcenv1) =
+        let discharge_pre tc =
+            let+ tc =
+              if   Option.is_some side
+              then EcLowGoal.t_intros_n 2 tc
+              else EcLowGoal.t_intros_n 1 tc
+            in
+            let+ tc = EcLowGoal.t_elim_and tc in
+            let+ tc = EcLowGoal.t_intro_s `Fresh tc in
+            let+ tc = EcLowGoal.t_elim_and tc in
+            let+ tc = EcLowGoal.t_intros_n ~clear:true 1 tc in
+            let+ tc = EcLowGoal.t_intro_s `Fresh tc in
+
+            t_id tc
+        in
+
         let pre = oget (EcLowPhlGoal.get_pre (FApi.tc1_goal tc)) in
         let post = oget (EcLowPhlGoal.get_post (FApi.tc1_goal tc)) in
         let eq, _, pre = destr_and3 pre in
         let tc = EcPhlConseq.t_conseq (f_and eq pre) post tc in
+        let tc = FApi.t_first discharge_pre tc in
 
         FApi.t_onall
           (EcLowGoal.t_clears names)