From 66cd741550db36479c8fe3a5b6cebce92ec7c64b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Winterhalter?= <theo.winterhalter@gmail.com>
Date: Mon, 5 Aug 2024 19:57:17 +0200
Subject: [PATCH] Use rasimpl more widely

---
 theories/Erasure.v     | 4 ++--
 theories/FreeTheorem.v | 4 ++--
 theories/Model.v       | 6 +++---
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/theories/Erasure.v b/theories/Erasure.v
index 789c9f6..487bff4 100644
--- 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
index b0a5bb9..e406dee 100644
--- 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
index 1b924bc..19e30d9 100644
--- 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 *)