frees_drops completed!

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / rtmap_after.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
index fef08518974b72a1862df14594b6d53d4446ad3a..4ca5caf746694bedf22ee49ee1ee1cf5444a8a0b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
@@ -13,7 +13,6 @@
 (**************************************************************************)
 
 include "ground_2/notation/relations/rafter_3.ma".
-include "ground_2/relocation/rtmap_sor.ma".
 include "ground_2/relocation/rtmap_istot.ma".
 
 (* RELOCATION MAP ***********************************************************)
@@ -271,8 +270,10 @@ lemma after_mono_eq: ∀f1,f2,f. f1 ⊚ f2 ≡ f → ∀g1,g2,g. g1 ⊚ g2 ≡ g
 lemma after_tls: ∀n,f1,f2,f. @⦃0, f1⦄ ≡ n → 
                  f1 ⊚ f2 ≡ f → ⫱*[n]f1 ⊚ f2 ≡ ⫱*[n]f.
 #n elim n -n //
-#n #IH #f1 #f2 #f #Hf1 #Hf cases (at_inv_pxn … Hf1) -Hf1 [ |*: // ]
-#g1 #Hg1 #H1 cases (after_inv_nxx … Hf … H1) -Hf /2 width=1 by/
+#n #IH #f1 #f2 #f #Hf1 #Hf
+cases (at_inv_pxn … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1
+cases (after_inv_nxx … Hf … H1) -Hf #g #Hg #H0 destruct
+<tls_xn <tls_xn /2 width=1 by/
 qed.
 
 (* Properties on isid *******************************************************)
@@ -339,32 +340,6 @@ lemma after_uni: ∀n1,n2. 𝐔❴n1❵ ⊚ 𝐔❴n2❵ ≡ 𝐔❴n1+n2❵.
 /4 width=5 by after_uni_next2, after_isid_sn, after_isid_dx, after_next/
 qed.
 
-(* Inversion lemmas on sor **************************************************)
-
-lemma sor_isid: ∀f1,f2,f. 𝐈⦃f1⦄ → 𝐈⦃f2⦄ → 𝐈⦃f⦄ → f1 ⋓ f2 ≡ f.
-/4 width=3 by sor_eq_repl_back2, sor_eq_repl_back1, isid_inv_eq_repl/ qed.
-(*
-lemma after_inv_sor: ∀f. 𝐅⦃f⦄ → ∀f2,f1. f2 ⊚ f1 ≡ f → ∀fa,fb. fa ⋓ fb ≡ f →
-                     ∃∃f1a,f1b. f2 ⊚ f1a ≡ fa & f2 ⊚ f1b ≡ fb & f1a ⋓ f1b ≡ f1.
-@isfin_ind
-[ #f #Hf #f2 #f1 #H1f #fa #fb #H2f
-  elim (after_inv_isid3 … H1f) -H1f //
-  elim (sor_inv_isid3 … H2f) -H2f //
-  /3 width=5 by ex3_2_intro, after_isid_sn, sor_isid/
-| #f #_ #IH #f2 #f1 #H1 #fa #fb #H2
-  elim (after_inv_xxp … H1) -H1 [ |*: // ] #g2 #g1 #H1f
-  elim (sor_inv_xxp … H2) -H2 [ |*: // ] #ga #gb #H2f
-  elim (IH … H1f … H2f) -f /3 width=11 by sor_pp, after_refl, ex3_2_intro/
-| #f #_ #IH #f2 #f1 #H1 #fa #fb #H2
-  elim (sor_inv_xxn … H2) -H2 [1,3,4: * |*: // ] #ga #gb #H2f
-  elim (after_inv_xxn … H1) -H1 [1,3,5,7,9,11: * |*: // ] #g2 [1,3,5: #g1 ] #H1f
-  elim (IH … H1f … H2f) -f
-  /3 width=11 by sor_np, sor_pn, sor_nn, after_refl, after_push, after_next, ex3_2_intro/
-  #x1a #x1b #H39 #H40 #H41 #H42 #H43 #H44
-  [ @ex3_2_intro
-    [3: /2 width=7 by after_next/ | skip
-    |5: @H41 | skip  
-*)
 (* Forward lemmas on at *****************************************************)
 
 lemma after_at_fwd: ∀i,i1,f. @⦃i1, f⦄ ≡ i → ∀f2,f1. f2 ⊚ f1 ≡ f →
@@ -439,10 +414,10 @@ lemma after_uni_dx: ∀i2,i1,f2. @⦃i1, f2⦄ ≡ i2 →
   elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
   [ #g2 #j1 #Hg2 #H1 #H2 destruct
     elim (after_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
-    /3 width=5 by after_next/
+    <tls_xn /3 width=5 by after_next/
   | #g2 #Hg2 #H2 destruct
     elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
-    /3 width=5 by after_next/
+    <tls_xn /3 width=5 by after_next/
   ]
 ]
 qed.
@@ -475,10 +450,10 @@ lemma after_uni_succ_dx: ∀i2,i1,f2. @⦃i1, f2⦄ ≡ i2 →
   elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
   [ #g2 #j1 #Hg2 #H1 #H2 destruct
     elim (after_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
-    /3 width=5 by after_next/
+    <tls_xn /3 width=5 by after_next/
   | #g2 #Hg2 #H2 destruct
     elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
-    /3 width=5 by after_next/
+    <tls_xn /3 width=5 by after_next/
   ]
 ]
 qed.