Use rasimpl more widely

TheoWinterhalter · Aug 5, 2024 · 66cd741 · 66cd741
1 parent a3ab7c8
commit 66cd741
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 7 deletions.
diff --git a/theories/Erasure.v b/theories/Erasure.v
@@ -314,7 +314,7 @@ Proof.
     2:{ eapply rscoping_upren. eassumption. }
     2:{ eapply rscoping_comp_upren. assumption. }
     destruct_ifs. all: try solve [ eauto ].
-    2:{ unfold close. ssimpl. cbn. unfold cty_lift. rasimpl. reflexivity. }
+    2:{ unfold close. rasimpl. cbn. unfold cty_lift. rasimpl. reflexivity. }
     rasimpl. unfold nones. rasimpl. reflexivity.
   - cbn.
     erewrite IHt1. 2,3: eassumption.
@@ -325,7 +325,7 @@ Proof.
     2:{ eapply rscoping_upren. eassumption. }
     2:{ eapply rscoping_comp_upren. assumption. }
     destruct_ifs. all: eauto.
-    unfold close. rasimpl. asimpl. reflexivity.
+    unfold close. rasimpl. reflexivity.
   - cbn.
     erewrite IHt1. 2,3: eassumption.
     erewrite IHt2. 2,3: eassumption.

diff --git a/theories/FreeTheorem.v b/theories/FreeTheorem.v
@@ -210,7 +210,7 @@ Proof.
       2:{
         eapply ccmeta_conv.
         - ertype. eapply ccmeta_conv. 1: ertype.
-          cbn. lhs_ssimpl. reflexivity.
+          cbn. rasimpl. unfold funcomp, shift. cbn. reflexivity.
         - cbn. reflexivity.
       }
       eapply ccmeta_conv.
@@ -230,7 +230,7 @@ Proof.
       2:{
         eapply ccmeta_conv.
         - ertype. eapply ccmeta_conv. 1: ertype.
-          cbn. lhs_ssimpl. reflexivity.
+          cbn. rasimpl. unfold shift, funcomp. cbn. reflexivity.
         - cbn. reflexivity.
       }
       eapply ccmeta_conv.

diff --git a/theories/Model.v b/theories/Model.v
@@ -131,11 +131,11 @@ Proof.
   - cbn. f_equal. 1: eauto.
     rewrite IHt2. apply ext_term.
     intros []. 1: reflexivity.
-    cbn. ssimpl. rewrite urm_ren. reflexivity.
+    cbn. unfold_funcomp. rewrite urm_ren. reflexivity.
   - cbn. f_equal. 1:eauto.
     rewrite IHt2. apply ext_term.
     intros []. 1: reflexivity.
-    cbn. ssimpl. rewrite urm_ren. reflexivity.
+    cbn. unfold_funcomp. rewrite urm_ren. reflexivity.
 Qed.
 
 Lemma urm_scoping :
@@ -256,7 +256,7 @@ Proof.
   - constructor.
   - constructor.
     + assumption.
-    + ssimpl. eapply urm_scoping. assumption.
+    + rasimpl. eapply urm_scoping. assumption.
 Qed.
 
 (* Conversion only requires the scope not the full context *)