jasmin-lang · rudynicolop · Jul 7, 2026 · Jul 7, 2026 · Jul 7, 2026 · Jul 7, 2026
diff --git a/AUTHORS b/AUTHORS
@@ -41,6 +41,7 @@ Pierre-Yves Strub
 Prema Narayan Ochoa
 Quentin Corradi
 Romain Tetley
+Rudy Peterson
 Santiago Arranz Olmos
 Simon Lukowski
 Swarn Priya

diff --git a/default.nix b/default.nix
@@ -33,7 +33,7 @@ let coqPackages =
       coq-elpi = super.coq-elpi.override { version = "master"; inherit elpi-version; };
       hierarchy-builder = super.hierarchy-builder.override { version = "master"; };
       ExtLib = super.ExtLib.override { version = "master"; };
-      paco = super.paco.override { version = "master"; };
+      rocq-coinduction = super.rocq-coinduction.override { version = "master"; };
       ITree = super.ITree.override { version = "master"; };
     })
   else coqPackages_9_0.overrideScope (self: super: {

diff --git a/opam b/opam
@@ -39,9 +39,14 @@ depends: [
   "coq-mathcomp-ssreflect" {>= "2.3" & < "2.6~"}
   "coq-mathcomp-algebra"
   "coq-mathcomp-word" {>= "3.4"}
-  "coq-paco"
-  "coq-itree"
+  "rocq-coinduction" { (= "1.21") }
+  "coq-itree" { (= "dev") }
 ]
 conflicts: [
   "ez-conf-lib"
 ]
+
+# Temporary "pin-depends" until a new ITree release with rocq-coinduction
+pin-depends: [
+  ["coq-itree.dev" "git+https://github.com/rudynicolop/InteractionTrees.git#61a470a7138666e2def022c2135268b2c5d9435d"]
+]
diff --git a/proofs/compiler/arm_lowering_proof.v b/proofs/compiler/arm_lowering_proof.v
@@ -1642,7 +1642,7 @@ Opaque esem.
     split => //.
     + rewrite /vars_lvals /read_rvs /vrvs /=; apply /disjointP.
       by move=> z hz; move/disjointP: hfvc => /(_ z); SvD.fsetdec.
-    by apply/hc/disjointP => z hz; move/disjointP: hfvc => /(_ z); SvD.fsetdec.
+    by apply hc; apply /disjointP => z hz; move/disjointP: hfvc => /(_ z); SvD.fsetdec.
   (* While *)
   + move=> al c e ii' c' hc hc' ii /disj_fvars_vars_I_Cwhile [/hc{}hc hfve /hc'{}hc'] /=.
     case heq: lower_condition => [pre e'].

diff --git a/proofs/compiler/array_copy_proof.v b/proofs/compiler/array_copy_proof.v
@@ -242,7 +242,7 @@ Transparent esem.
     rewrite /= get_var_neq; last by move=> [? _]; subst ty.
     rewrite /= /get_var hx /= truncate_word_u /=.
     by rewrite hset /= write_var_eq_type.
-  move=> /(_ n _ vm1' tx0 hvm1' htx0) [] //; first by lia.
+  move=> /(_ n _ vm1' tx0 hvm1' htx0) [] //. (*first by lia.*)
   + by rewrite Z.sub_diag.
   rewrite Z.sub_diag => vm2 [] hvm2 htx' hfor; exists vm2; split.
   + apply: uincl_onT.

diff --git a/proofs/compiler/array_init_proof.v b/proofs/compiler/array_init_proof.v
@@ -94,7 +94,9 @@ Proof.
   + by move=> > hc ii; apply wequiv_for_rel_uincl with checker_st_uincl tt tt.
   + by move=> > ?? ii; apply wequiv_while_rel_uincl with checker_st_uincl tt.
   move=> xs fn es ii; apply wequiv_call_rel_uincl with checker_st_uincl tt => //.
- move=> ???; exact/wequiv_fun_rec.
+  move=> fs1 fs2 ?.
+  change fs_uincl with (rpostF fn fn fs1 fs2).
+  by apply wequiv_fun_rec.
 Qed.
 
 End IT_REMOVE_INIT.
@@ -236,7 +238,7 @@ Proof.
    apply wequiv_cat with (cmpl_inv I').
    + by have /= := hi I; rewrite heqi.
    by have /= := hc I'; rewrite heqc.
- 1-4, 6-8: by move=> * ii I; apply/it_aux.
+ 1-4, 6-8: by move=> * ii I; apply it_aux.
  move=> e c1 c2 hc1 hc2 ii I /=.
  case heq1 : add_init_c => [c1' I1].
  case heq2 : add_init_c => [c2' I2] /=.

diff --git a/proofs/compiler/dead_code_proof.v b/proofs/compiler/dead_code_proof.v
@@ -198,7 +198,7 @@ Section PROOF.
     apply: rbindP => // [[s' sci]] h.
     case: (boolP (Sv.subset _ _)) => //=.
     + move=> /Sv.subset_spec Hsub k; apply ok_inj in k; subst.
-      exists s, s'; split; auto. SvD.fsetdec.
+      exists s, s'; split; auto. (*SvD.fsetdec.*)
     move=> _ hloop; case: (ih _ hloop) => si [si'] [Hsub] [h' le].
     exists si, si'; split; auto. SvD.fsetdec.
   Qed.

diff --git a/proofs/compiler/inline_proof.v b/proofs/compiler/inline_proof.v
@@ -354,7 +354,9 @@ Proof using uniq_funname inline_fd_ok.
     + by split => //; rewrite !read_writeE; clear; SvD.fsetdec.
     + by split => //; rewrite !read_writeE; clear; SvD.fsetdec.
     move=> i1 i2 h; rewrite /= /do_inline eqxx hinline /=.
-    exact/(wequiv_fun_rec (p1 := p1) (p2 := p2)).
+    change fs_uincl with (rpostF f f i1 i2).
+    now eapply (wequiv_fun_rec (p1 := p1) (p2 := p2)
+                  (ev1:=p1.(p_extra)) (ev2:=p2.(p_extra))).
   rewrite /check_disjoint.
   t_xrbindP => ffd /get_funP hffd.
   case: ifP => // hdisj _ ? <-.

diff --git a/proofs/compiler/it_linearization_proof.v b/proofs/compiler/it_linearization_proof.v
@@ -3,7 +3,7 @@
 From Coq
 Require Import Setoid Morphisms Lia.
 
-Require Import Paco.paco.
+Require Import Coinduction.all.
 
 From ITree Require Import
   ITree
@@ -1934,7 +1934,6 @@ Proof.
   + by have := hc _ _ _ _ _ _ pc hfn'; rewrite size_cat => /(_ hpc'); apply.
   move=> ls'' _ [<- ? hpc''].
   rewrite mix_ilsteps_b0 => //; last by rewrite hpc''; simpl_size; lia.
-  by apply eqit_Ret.
 Qed.
 
 Lemma linear_c_end_cons : ∀ (i : instr) (c : cmd), Pi i → Pc c → Pc (i :: c).
@@ -2275,7 +2274,7 @@ Lemma mix_ilsteps_add_align P ii al lc Q ls :
         (setcpc ls fn (size P + size (add_align ii al [::]))).
 Proof.
   case: al => /= hfn hpc C; last first.
-  + by rewrite addn0 -hpc -hfn /setcpc; case: (ls) => /= >; reflexivity.
+  + rewrite addn0 -hpc -hfn /setcpc; case: (ls) => /= *; reflexivity.
   rewrite (step_mix_ilsteps C) //=; last by simpl_size;lia.
   rewrite /lnext_pc /setcpc addn1 hfn hpc; reflexivity.
 Qed.
@@ -2349,21 +2348,21 @@ Proof.
       (* Here the proof is done by coinduction *)
       have {}ih1 := ih1 _ _ _ _ _ pre1.
       have {}ih2 := ih2 _ _ _ _ _ pre2.
-      move=> {hfn hpc}; move: ls; ginit; gcofix SELF => s.
+      move=> {hfn hpc}; move: ls; coinduction ch SELF => s.
       rewrite unfold_iter bind_bind.
       rewrite (mix_ilsteps_split p' (pcs':=size P1) (pce':=size P1 + size lc1));[| rewrite /P1; simpl_size; lia..].
-      guclo eqit_clo_bind.
-      econstructor.
+      ebind.
       + have -> : lnext_pc (setcpc s fn (size P + size lialign)) = setcpc s fn (size P1).
         + rewrite /lnext_pc /setcpc /P1 /=; f_equal; simpl_size; lia.
+        apply (@gfp_bchain _ _ (eqit_mon _ _)).
         by apply ih1.
       move=> ls1 _ [<- hfn1 hpc1]; rewrite bind_bind.
       rewrite (mix_ilsteps_split p' (pcs':=size P2) (pce':=size P2 + size lc2));[| rewrite /P2; simpl_size; lia..].
-      guclo eqit_clo_bind.
-      econstructor.
+      ebind.
       + have -> : ls1 = (setcpc ls1 fn (size P2)).
         + rewrite /setcpc /P2 /P1 /=. case: ls1 hfn1 hpc1 => /= > -> ->.
           f_equal; simpl_size; lia.
+        apply (@gfp_bchain _ _ (eqit_mon _ _)).
         by apply ih2.
       move=> ls2 _ [<- hfn2 hpc2]; rewrite bind_ret_l.
       rewrite catA in C2.
@@ -2372,7 +2371,7 @@ Proof.
       rewrite find_label_cat_hd; last first.
       + apply: (disjoint_labels_cat D); rewrite /lialign; case: (al) => //; lia.
       rewrite find_labelE /lilabel /is_label /= eqxx /=.
-      gstep; constructor; gfinal; left.
+      etau.
       have -> : setcpc ls2 fn (size (P ++ lialign) + 0).+1 =
                 lnext_pc (setcpc ls2 fn (size P + size lialign)).
       + rewrite /setcpc /lnext_pc /=; f_equal; simpl_size; lia.
@@ -2441,36 +2440,35 @@ Proof.
     rewrite -/lialign (step_mix_ilsteps C) //=; [ | by rewrite /lialign; simpl_size;lia..].
     (* Here the proof is done by coinduction *)
     have {}ih1 := ih1 _ _ _ _ _ pre1.
-    move=> {hfn hpc}; move: ls; ginit; gcofix SELF => s.
+    move=> {hfn hpc}; move: ls; coinduction ch SELF => s.
     rewrite unfold_iter bind_bind.
     rewrite (mix_ilsteps_split p' (pcs':=size P1) (pce':=size P1 + size lc1));[| rewrite /P1; simpl_size; lia..].
-    guclo eqit_clo_bind.
-    econstructor.
+    ebind.
     + have -> : lnext_pc (setcpc s fn (size P + size lialign)) = setcpc s fn (size P1).
       + rewrite /lnext_pc /setcpc /P1 /=; f_equal; simpl_size; lia.
+      apply (@gfp_bchain _ _ (eqit_mon _ _)).
       by apply ih1.
     move=> ls1 _ [<- hfn1 hpc1].
     rewrite catA in C1.
-    rewrite (step_mix_ilsteps_eq_itree C1) //=; [|rewrite /P1 ?hpc1; simpl_size; lia..].
-    rewrite /eval_instr /=.
-    case: (Let v := sem_fexpr _ _ in to_bool v) => [b | err] /=; last first.
-    + rewrite bind_throw; apply gpaco2_mon with bot2 bot2 => //.
-      gfinal; right; rewrite -/(eqit eq true true); reflexivity.
+    rewrite (step_mix_ilsteps_eq_itree C1) //; try bcbn; [|rewrite /P1 ?hpc1; simpl_size; lia..].
+    rewrite /eval_instr. bcbn.
+    case: (Let v := sem_fexpr _ _ in to_bool v) => [b | err]; bcbn; last first.
+    + constructor; intros [].
     rewrite hfn1 (eval_jumpE C).
     rewrite find_label_cat_hd; last first.
     + apply: (disjoint_labels_cat D); rewrite /lialign; case: (al) => //; lia.
-    rewrite find_labelE /lilabel /is_label /= eqxx /=.
+    rewrite find_labelE /lilabel /is_label; bcbn. rewrite positive_eqb_refl. bcbn.
     case: b.
     + rewrite bind_bind (mix_ilsteps_b0 p' (size P2)) //; last first.
       + by rewrite /setcpc /=; simpl_size;lia.
-      rewrite !bind_ret_l; gstep; constructor; gfinal; left.
+      rewrite !bind_ret_l; etau.
       have -> : setcpc ls1 fn (size (P ++ lialign) + 0).+1 =
                 lnext_pc (setcpc (setcpc ls1 fn (size P2)) fn (size P + size lialign)).
       + rewrite /setcpc /lnext_pc /P2 /=; f_equal; simpl_size; lia.
       apply SELF.
     rewrite bind_ret_l mix_ilsteps_b0 //; last first.
     + by rewrite /lnext_pc hpc1 /P1 /=;simpl_size;lia.
-    setoid_rewrite tau_euttge; gstep; constructor.
+    setoid_rewrite tau_euttge. eret.
     by rewrite /lnext_pc /setcpc hpc1 /P1 /=; f_equal => //; simpl_size; lia.
 
   (* The general case *)
@@ -2521,43 +2519,43 @@ Proof.
   (* Here the proof is done by coinduction *)
   have {}ih1 := ih1 _ _ _ _ _ pre1.
   have {}ih2 := ih2 _ _ _ _ _ pre2.
-  rewrite hfn; move=> {hpc hfn}; move: ls; ginit; gcofix SELF => s.
+  rewrite hfn; move=> {hpc hfn}; move: ls; coinduction ch SELF => s.
   rewrite unfold_iter bind_bind.
   rewrite (mix_ilsteps_split p' (pcs':=size P1) (pce':=size P1 + size lc1));[| rewrite /P1; simpl_size; lia..].
-  guclo eqit_clo_bind; econstructor.
+  ebind.
   + have -> : setcpc s fn (size P + (size lialign + (size lc2 + 0).+1).+1).+1 =
               setcpc s fn (size P1).
     + rewrite /lnext_pc /setcpc /P1 /P2 /=; f_equal => //; simpl_size; lia.
+    eapply (@gfp_bchain _ _ (eqit_mon _ _)).
     by apply ih1.
   move=> ls1 _ [<- hfn1 hpc1].
   rewrite catA in C1.
-  rewrite (step_mix_ilsteps_eq_itree C1) //=; [|rewrite /P1 ?hpc1; simpl_size; lia..].
-  rewrite /eval_instr /=.
-  case: (Let v := sem_fexpr _ _ in to_bool v) => [b | err] /=; last first.
-  + rewrite bind_throw; apply gpaco2_mon with bot2 bot2 => //.
-    gfinal; right; rewrite -/(eqit eq true true); reflexivity.
+  rewrite (step_mix_ilsteps_eq_itree C1) //; try bcbn; [|rewrite /P1 ?hpc1; simpl_size; lia..].
+  rewrite /eval_instr. bcbn.
+  case: (Let v := sem_fexpr _ _ in to_bool v) => [b | err]; bcbn; last first.
+  + constructor; intros [].
   rewrite hfn1 (eval_jumpE C).
   rewrite find_label_cat_hd; last by apply: D; lia.
-  rewrite find_labelE /= -!catA find_label_cat_hd; last by rewrite /lialign; case: (al).
-  rewrite find_labelE /is_label /= eqxx /=.
+  rewrite find_labelE; bcbn; rewrite -!catA find_label_cat_hd; last by rewrite /lialign; case: (al).
+  rewrite find_labelE /is_label. bcbn. rewrite positive_eqb_refl. bcbn.
   case: b.
   + rewrite bind_bind; setoid_rewrite tau_euttge.
     rewrite (mix_ilsteps_split p' (pcs':=size P2) (pce':=size P2 + size lc2));[| rewrite /P2; simpl_size; lia..].
-    guclo eqit_clo_bind.
-    econstructor.
+    ebind.
     + have -> : setcpc ls1 fn (size P + (size lialign + 0).+1).+1 = setcpc ls1 fn (size P2).
       + rewrite /setcpc /P2 /=; f_equal; simpl_size; lia.
+      eapply (@gfp_bchain _ _ (eqit_mon _ _)).
       by apply ih2.
     move=> ls2 _ [<- hfn2 hpc2]; rewrite bind_ret_l.
     rewrite catA in C2; rewrite (step_mix_ilsteps_eq_itree C2) //=;[|rewrite ?hpc2 /P2 /Q2; simpl_size; lia..].
-    gstep; constructor; gfinal; left.
+    etau.
     have -> : lnext_pc ls2 = setcpc ls2 fn (size P + (size lialign + (size lc2 + 0).+1).+1).+1.
     + rewrite /lnext_pc /setcpc hpc2 /P2; f_equal => //; simpl_size; lia.
     by apply SELF.
   rewrite bind_ret_l; setoid_rewrite tau_euttge.
   rewrite mix_ilsteps_b0 //; last first.
   + by rewrite /lnext_pc hpc1 /P1 /=;simpl_size;lia.
-  gstep; constructor.
+  eret.
   by rewrite /lnext_pc /setcpc hpc1 /P1 /=; f_equal => //; simpl_size; lia.
 Qed.
 
@@ -3256,10 +3254,10 @@ End ILSTEPS_END.
     rewrite (sem_fexpr_bool hinv chk_e hb) /=; rewrite -(bind_ret_r (isem_cmd_ _ _ _ _)) => {hb}; case: b.
     + have {}ih1:= ih1 _ _ _ _ _ hpre1 (Sv.empty, s1) (setcpc ls1 fn (size P1)) (inv_c_setpc hinv erefl).
       apply (xrutt_facts.xrutt_bind ih1) => ks2 ls2 hpost.
-      by apply/xrutt.xrutt_Ret/post_c_post_ir/(post_c_setpc hpost); rewrite size_cat.
+      by apply xrutt.xrutt_Ret, post_c_post_ir, (post_c_setpc hpost); rewrite size_cat.
     have {}ih2:= ih2 _ _ _ _ _ hpre2 (Sv.empty, s1) (setcpc ls1 fn (size P2)) (inv_c_setpc hinv erefl).
     apply (xrutt_facts.xrutt_bind ih2) => ks2 ls2 hpost.
-    by apply/xrutt.xrutt_Ret/post_c_post_ir/(post_c_setpc hpost); rewrite size_cat.
+    by apply xrutt.xrutt_Ret, post_c_post_ir, (post_c_setpc hpost); rewrite size_cat.
   Qed.
 
   Lemma Hfor : ∀ (v : var_i) (dir : expr.dir) (lo hi : pexpr) (c : cmd), Pc c → Pi_r (Cfor v (dir, lo, hi) c).
@@ -3292,11 +3290,11 @@ End ILSTEPS_END.
       by rewrite (sem_fexpr_bool (post_c_inv_c hpost2) chk_e hb).
     have hpost2' := post_c_trans hpost1 hpost2.
     case: b hpre2 => hpre2; last first.
-    + apply/xrutt.xrutt_Ret;constructor.
-      by apply/post_c_post_ir /(post_c_setpc hpost2'); rewrite size_cat.
+    + apply xrutt.xrutt_Ret;constructor.
+      by apply post_c_post_ir, (post_c_setpc hpost2'); rewrite size_cat.
     have {}ih2:= ih2 _ _ _ _ _ (hpre2 erefl) ks2 (setcpc ls2 fn (size P2)) (post_c_inv_c (post_c_setpc hpost2 erefl)).
     apply (xrutt_facts.xrutt_bind ih2) => ks3 ls3 hpost3.
-    apply/xrutt.xrutt_Ret;constructor.
+    apply xrutt.xrutt_Ret;constructor.
     exists (P2 ++ lc2); apply: post_c_trans hpost2' hpost3.
   Qed.
 
@@ -4073,7 +4071,7 @@ End ILSTEPS_END.
 (* FIXME: move this *)
 Lemma mix_ilsteps_split_handle_call_cond P lc lbody fn ls :
   is_linear_of fn lbody ->
-  size P + size lc <= size lbody ->
+  (size P + size lc <= size lbody)%nat ->
   mix_ilsteps p' (handle_call_cond p' fn) ls ≅
   ITree.bind (mix_ilsteps p' (pc_between_c fn P lc) ls)
        (mix_ilsteps p' (handle_call_cond p' fn)).
@@ -4865,7 +4863,7 @@ Qed.
         + (* ra_call = None, easy case: mi = m1 *)
           exists (lmem t1); split=> //.
           rewrite mix_ilsteps_b0 // /P2 /=.
-          rewrite -hfn -hpc; case: (t1) => >; reflexivity.
+          rewrite -hfn -hpc; case: (t1) => *; reflexivity.
         (* ra_call = Some _ *)
         (* TODO this should be a lemma it is used elsewhere (above)*)
         have [m1s ok_m1s M']:

diff --git a/proofs/compiler/it_tunneling_proof.v b/proofs/compiler/it_tunneling_proof.v
@@ -409,7 +409,7 @@ Lemma tunnel_cmd endpc s :
   eqit eq true true (ilsem p' (untilpc endpc) s) (ilsem p (untilpc endpc) s).
 Proof using pp'.
   move=> hend.
-  apply while.eqit_iter_n with eq => //.
+  apply while.eutt_iter_n with eq => //.
   move=> {}s _ <-.
   setoid_rewrite i_lsem_body_n; setoid_rewrite i_lsem_body.
   rewrite /lsem_body /untilpc; case: eqP.

diff --git a/proofs/compiler/lower_spill_proof.v b/proofs/compiler/lower_spill_proof.v
@@ -466,7 +466,7 @@ Proof using spill_prog_ok.
     exists s.
     + by move: hinit; rewrite /initialize_funcall /= eq_p_extra.
     exists (st_eq tt), (st_eq tt); split => //.
-    + by apply/wequiv_rec_st_eq/eq_globs.
+    + by apply wequiv_rec_st_eq, eq_globs.
     by apply st_eq_finalize.
   case ok_m: init_map => [ m _count ].
   t_xrbindP => _.
@@ -555,7 +555,7 @@ Proof using spill_prog_ok.
   apply wequiv_call_rel_eq with (checker_st_ve S) env => //.
   + split => //; clear -hsub; SvD.fsetdec.
   + split => //; clear -hsub; SvD.fsetdec.
-  move=> fs fs' <-; exact/wequiv_fun_rec.
+  move=> fs fs' <-; by apply (wequiv_fun_rec (spec:=eq_spec)).
 Qed.
 
 End IT.

diff --git a/proofs/compiler/makeReferenceArguments_proof.v b/proofs/compiler/makeReferenceArguments_proof.v
@@ -523,7 +523,7 @@ Context
     rewrite /isem_pexprs eval_args' /= Eqit.bind_ret_l Eqit.bind_bind.
     set fs1 := mk_fstate ves s; set fs2 := mk_fstate ves (with_vm s vmx).
     apply xrutt_facts.xrutt_bind with (rpostF (eS:=mra_spec) f f fs1 fs2);
-      first exact/(wequiv_fun_rec (ev1 := ev) (ev2 := ev)).
+      first by eapply (wequiv_fun_rec (p1:=p) (p2:=p) (ev1 := ev) (ev2 := ev)).
     move=> fr _[<-]; rewrite heq => -[_ [<-] [vres' htr]].
     rewrite /upd_estate.
     case h3 : write_lvals => [s' | e /=]; last first.

diff --git a/proofs/compiler/remove_assert_proof.v b/proofs/compiler/remove_assert_proof.v
@@ -77,7 +77,7 @@ Section REMOVE_ASSERT.
       by apply wequiv_while_rel_eq with checker_ra_eq tt.
     move=> >.
     apply wequiv_call_rel_eq_wa with checker_ra_eq tt => //.
-    move=> ?? <-; exact/wequiv_fun_rec.
+    move=> ?? <-; by apply (wequiv_fun_rec (spec:=eq_spec)).
   Qed.
 
 End REMOVE_ASSERT.
diff --git a/proofs/compiler/stack_alloc_proof_2.v b/proofs/compiler/stack_alloc_proof_2.v
@@ -2907,9 +2907,8 @@ Proof.
   + move=> /andP [hincl1 hincl2] [<- <- <- <- <-].
     exists table, rmap, table2, rmap2; split=> //.
     + by apply incl_table_refl.
-    + by split.
     + by apply Incl_refl.
-    by left.
+    + eauto.
   have h : wf_table_vars table rmap /\ Sv.Subset (vars table) (vars table) by split.
   have [hwf hsub]:= wf_table_vars_merge h h2.
   move=> _ /hrec{} [] //.

diff --git a/proofs/compiler/stack_zeroization_proof.v b/proofs/compiler/stack_zeroization_proof.v
@@ -1,5 +1,3 @@
-From Paco Require Import paco.
-
 From ITree Require Import
   ITree
   ITreeFacts

diff --git a/proofs/compiler/x86_lowering_proof.v b/proofs/compiler/x86_lowering_proof.v
@@ -1876,7 +1876,7 @@ Section PROOF.
       split => //.
       + rewrite /vars_lvals /read_rvs /vrvs /=; apply /disjointP.
         by move=> z hz; move/disjointP: hfvc => /(_ z); clear -hz; SvD.fsetdec.
-      by apply/hc/disjointP => z hz; move/disjointP: hfvc => /(_ z); clear -hz; SvD.fsetdec.
+      by apply hc; apply/disjointP => z hz; move/disjointP: hfvc => /(_ z); clear -hz; SvD.fsetdec.
     (* While *)
     + move=> al c e ii' c' hc hc' ii /disj_fvars_vars_I_Cwhile [/hc{}hc hfve /hc'{}hc'] /=.
       case heq: lower_condition => [pre e'].