renaming in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / drops.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
index fdcf1a70f3b101479da3e09ca63313ccb67fe4e7..f982cb1a65bb4f43dd62f3385fa2b8d8da9a0a97 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
@@ -15,7 +15,7 @@
 include "ground_2/relocation/rtmap_coafter.ma".
 include "basic_2/notation/relations/rdropstar_3.ma".
 include "basic_2/notation/relations/rdropstar_4.ma".
-include "basic_2/relocation/lreq.ma".
+include "basic_2/relocation/seq.ma".
 include "basic_2/relocation/lifts_bind.ma".
 
 (* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
@@ -26,10 +26,10 @@ include "basic_2/relocation/lifts_bind.ma".
 *)
 inductive drops (b:bool): rtmap → relation lenv ≝
 | drops_atom: ∀f. (b = Ⓣ → 𝐈⦃f⦄) → drops b (f) (⋆) (⋆)
-| drops_drop: â\88\80f,I,L1,L2. drops b f L1 L2 â\86\92 drops b (⫯f) (L1.ⓘ{I}) L2
+| drops_drop: â\88\80f,I,L1,L2. drops b f L1 L2 â\86\92 drops b (â\86\91f) (L1.ⓘ{I}) L2
 | drops_skip: ∀f,I1,I2,L1,L2.
               drops b f L1 L2 → ⬆*[f] I2 ≘ I1 →
-              drops b (â\86\91f) (L1.ⓘ{I1}) (L2.ⓘ{I2})
+              drops b (⫯f) (L1.ⓘ{I1}) (L2.ⓘ{I2})
 .
 
 interpretation "uniform slicing (local environment)"
@@ -160,7 +160,7 @@ qed-.
 lemma drops_inv_atom1: ∀b,f,Y. ⬇*[b, f] ⋆ ≘ Y → Y = ⋆ ∧ (b = Ⓣ → 𝐈⦃f⦄).
 /2 width=3 by drops_inv_atom1_aux/ qed-.
 
-fact drops_inv_drop1_aux: â\88\80b,f,X,Y. â¬\87*[b, f] X â\89\98 Y â\86\92 â\88\80g,I,K. X = K.â\93\98{I} â\86\92 f = ⫯g →
+fact drops_inv_drop1_aux: â\88\80b,f,X,Y. â¬\87*[b, f] X â\89\98 Y â\86\92 â\88\80g,I,K. X = K.â\93\98{I} â\86\92 f = â\86\91g →
                           ⬇*[b, g] K ≘ Y.
 #b #f #X #Y * -f -X -Y
 [ #f #Hf #g #J #K #H destruct
@@ -171,10 +171,10 @@ qed-.
 
 (* Basic_1: includes: drop_gen_drop *)
 (* Basic_2A1: includes: drop_inv_drop1_lt drop_inv_drop1 *)
-lemma drops_inv_drop1: â\88\80b,f,I,K,Y. â¬\87*[b, ⫯f] K.ⓘ{I} ≘ Y → ⬇*[b, f] K ≘ Y.
+lemma drops_inv_drop1: â\88\80b,f,I,K,Y. â¬\87*[b, â\86\91f] K.ⓘ{I} ≘ Y → ⬇*[b, f] K ≘ Y.
 /2 width=6 by drops_inv_drop1_aux/ qed-.
 
-fact drops_inv_skip1_aux: â\88\80b,f,X,Y. â¬\87*[b, f] X â\89\98 Y â\86\92 â\88\80g,I1,K1. X = K1.â\93\98{I1} â\86\92 f = â\86\91g →
+fact drops_inv_skip1_aux: â\88\80b,f,X,Y. â¬\87*[b, f] X â\89\98 Y â\86\92 â\88\80g,I1,K1. X = K1.â\93\98{I1} â\86\92 f = ⫯g →
                           ∃∃I2,K2. ⬇*[b, g] K1 ≘ K2 & ⬆*[g] I2 ≘ I1 & Y = K2.ⓘ{I2}.
 #b #f #X #Y * -f -X -Y
 [ #f #Hf #g #J1 #K1 #H destruct
@@ -186,11 +186,11 @@ qed-.
 
 (* Basic_1: includes: drop_gen_skip_l *)
 (* Basic_2A1: includes: drop_inv_skip1 *)
-lemma drops_inv_skip1: â\88\80b,f,I1,K1,Y. â¬\87*[b, â\86\91f] K1.ⓘ{I1} ≘ Y →
+lemma drops_inv_skip1: â\88\80b,f,I1,K1,Y. â¬\87*[b, ⫯f] K1.ⓘ{I1} ≘ Y →
                        ∃∃I2,K2. ⬇*[b, f] K1 ≘ K2 & ⬆*[f] I2 ≘ I1 & Y = K2.ⓘ{I2}.
 /2 width=5 by drops_inv_skip1_aux/ qed-.
 
-fact drops_inv_skip2_aux: â\88\80b,f,X,Y. â¬\87*[b, f] X â\89\98 Y â\86\92 â\88\80g,I2,K2. Y = K2.â\93\98{I2} â\86\92 f = â\86\91g →
+fact drops_inv_skip2_aux: â\88\80b,f,X,Y. â¬\87*[b, f] X â\89\98 Y â\86\92 â\88\80g,I2,K2. Y = K2.â\93\98{I2} â\86\92 f = ⫯g →
                           ∃∃I1,K1. ⬇*[b, g] K1 ≘ K2 & ⬆*[g] I2 ≘ I1 & X = K1.ⓘ{I1}.
 #b #f #X #Y * -f -X -Y
 [ #f #Hf #g #J2 #K2 #H destruct
@@ -202,14 +202,14 @@ qed-.
 
 (* Basic_1: includes: drop_gen_skip_r *)
 (* Basic_2A1: includes: drop_inv_skip2 *)
-lemma drops_inv_skip2: â\88\80b,f,I2,X,K2. â¬\87*[b, â\86\91f] X ≘ K2.ⓘ{I2} →
+lemma drops_inv_skip2: â\88\80b,f,I2,X,K2. â¬\87*[b, ⫯f] X ≘ K2.ⓘ{I2} →
                        ∃∃I1,K1. ⬇*[b, f] K1 ≘ K2 & ⬆*[f] I2 ≘ I1 & X = K1.ⓘ{I1}.
 /2 width=5 by drops_inv_skip2_aux/ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
 fact drops_fwd_drop2_aux: ∀b,f2,X,Y. ⬇*[b, f2] X ≘ Y → ∀I,K. Y = K.ⓘ{I} →
-                          â\88\83â\88\83f1,f. ð\9d\90\88â¦\83f1â¦\84 & f2 â\8a\9a ⫯f1 ≘ f & ⬇*[b, f] X ≘ K.
+                          â\88\83â\88\83f1,f. ð\9d\90\88â¦\83f1â¦\84 & f2 â\8a\9a â\86\91f1 ≘ f & ⬇*[b, f] X ≘ K.
 #b #f2 #X #Y #H elim H -f2 -X -Y
 [ #f2 #Hf2 #J #K #H destruct
 | #f2 #I #L1 #L2 #_ #IHL #J #K #H elim (IHL … H) -IHL
@@ -220,7 +220,7 @@ fact drops_fwd_drop2_aux: ∀b,f2,X,Y. ⬇*[b, f2] X ≘ Y → ∀I,K. Y = K.ⓘ
 qed-.
 
 lemma drops_fwd_drop2: ∀b,f2,I,X,K. ⬇*[b, f2] X ≘ K.ⓘ{I} →
-                       â\88\83â\88\83f1,f. ð\9d\90\88â¦\83f1â¦\84 & f2 â\8a\9a ⫯f1 ≘ f & ⬇*[b, f] X ≘ K.
+                       â\88\83â\88\83f1,f. ð\9d\90\88â¦\83f1â¦\84 & f2 â\8a\9a â\86\91f1 ≘ f & ⬇*[b, f] X ≘ K.
 /2 width=4 by drops_fwd_drop2_aux/ qed-.
 
 (* Properties with test for identity ****************************************)
@@ -244,7 +244,7 @@ lemma drops_fwd_isid: ∀b,f,L1,L2. ⬇*[b, f] L1 ≘ L2 → 𝐈⦃f⦄ → L1
 qed-.
 
 lemma drops_after_fwd_drop2: ∀b,f2,I,X,K. ⬇*[b, f2] X ≘ K.ⓘ{I} →
-                             â\88\80f1,f. ð\9d\90\88â¦\83f1â¦\84 â\86\92 f2 â\8a\9a ⫯f1 ≘ f → ⬇*[b, f] X ≘ K.
+                             â\88\80f1,f. ð\9d\90\88â¦\83f1â¦\84 â\86\92 f2 â\8a\9a â\86\91f1 ≘ f → ⬇*[b, f] X ≘ K.
 #b #f2 #I #X #K #H #f1 #f #Hf1 #Hf elim (drops_fwd_drop2 … H) -H
 #g1 #g #Hg1 #Hg #HK lapply (after_mono_eq … Hg … Hf ??) -Hg -Hf
 /3 width=5 by drops_eq_repl_back, isid_inv_eq_repl, eq_next/
@@ -269,7 +269,7 @@ qed-.
 
 lemma drops_inv_isuni: ∀f,L1,L2. ⬇*[Ⓣ, f] L1 ≘ L2 → 𝐔⦃f⦄ →
                        (𝐈⦃f⦄ ∧ L1 = L2) ∨
-                       â\88\83â\88\83g,I,K. â¬\87*[â\93\89, g] K â\89\98 L2 & ð\9d\90\94â¦\83gâ¦\84 & L1 = K.â\93\98{I} & f = ⫯g.
+                       â\88\83â\88\83g,I,K. â¬\87*[â\93\89, g] K â\89\98 L2 & ð\9d\90\94â¦\83gâ¦\84 & L1 = K.â\93\98{I} & f = â\86\91g.
 #f #L1 #L2 * -f -L1 -L2
 [ /4 width=1 by or_introl, conj/
 | /4 width=7 by isuni_inv_next, ex4_3_intro, or_intror/
@@ -280,7 +280,7 @@ qed-.
 (* Basic_2A1: was: drop_inv_O1_pair1 *)
 lemma drops_inv_bind1_isuni: ∀b,f,I,K,L2. 𝐔⦃f⦄ → ⬇*[b, f] K.ⓘ{I} ≘ L2 →
                              (𝐈⦃f⦄ ∧ L2 = K.ⓘ{I}) ∨
-                             â\88\83â\88\83g. ð\9d\90\94â¦\83gâ¦\84 & â¬\87*[b, g] K â\89\98 L2 & f = ⫯g.
+                             â\88\83â\88\83g. ð\9d\90\94â¦\83gâ¦\84 & â¬\87*[b, g] K â\89\98 L2 & f = â\86\91g.
 #b #f #I #K #L2 #Hf #H elim (isuni_split … Hf) -Hf * #g #Hg #H0 destruct
 [ lapply (drops_inv_skip1 … H) -H * #Z #Y #HY #HZ #H destruct
   <(drops_fwd_isid … HY Hg) -Y >(liftsb_fwd_isid … HZ Hg) -Z
@@ -292,7 +292,7 @@ qed-.
 (* Basic_2A1: was: drop_inv_O1_pair2 *)
 lemma drops_inv_bind2_isuni: ∀b,f,I,K,L1. 𝐔⦃f⦄ → ⬇*[b, f] L1 ≘ K.ⓘ{I} →
                              (𝐈⦃f⦄ ∧ L1 = K.ⓘ{I}) ∨
-                             â\88\83â\88\83g,I1,K1. ð\9d\90\94â¦\83gâ¦\84 & â¬\87*[b, g] K1 â\89\98 K.â\93\98{I} & L1 = K1.â\93\98{I1} & f = ⫯g.
+                             â\88\83â\88\83g,I1,K1. ð\9d\90\94â¦\83gâ¦\84 & â¬\87*[b, g] K1 â\89\98 K.â\93\98{I} & L1 = K1.â\93\98{I1} & f = â\86\91g.
 #b #f #I #K *
 [ #Hf #H elim (drops_inv_atom1 … H) -H #H destruct
 | #L1 #I1 #Hf #H elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
@@ -302,7 +302,7 @@ lemma drops_inv_bind2_isuni: ∀b,f,I,K,L1. 𝐔⦃f⦄ → ⬇*[b, f] L1 ≘ K.
 ]
 qed-.
 
-lemma drops_inv_bind2_isuni_next: â\88\80b,f,I,K,L1. ð\9d\90\94â¦\83fâ¦\84 â\86\92 â¬\87*[b, ⫯f] L1 ≘ K.ⓘ{I} →
+lemma drops_inv_bind2_isuni_next: â\88\80b,f,I,K,L1. ð\9d\90\94â¦\83fâ¦\84 â\86\92 â¬\87*[b, â\86\91f] L1 ≘ K.ⓘ{I} →
                                   ∃∃I1,K1. ⬇*[b, f] K1 ≘ K.ⓘ{I} & L1 = K1.ⓘ{I1}.
 #b #f #I #K #L1 #Hf #H elim (drops_inv_bind2_isuni … H) -H /2 width=3 by isuni_next/ -Hf *
 [ #H elim (isid_inv_next … H) -H //
@@ -341,7 +341,7 @@ qed-.
 
 (* Basic_1: was: drop_S *)
 (* Basic_2A1: was: drop_fwd_drop2 *)
-lemma drops_isuni_fwd_drop2: â\88\80b,f,I,X,K. ð\9d\90\94â¦\83fâ¦\84 â\86\92 â¬\87*[b, f] X â\89\98 K.â\93\98{I} â\86\92 â¬\87*[b, ⫯f] X ≘ K.
+lemma drops_isuni_fwd_drop2: â\88\80b,f,I,X,K. ð\9d\90\94â¦\83fâ¦\84 â\86\92 â¬\87*[b, f] X â\89\98 K.â\93\98{I} â\86\92 â¬\87*[b, â\86\91f] X ≘ K.
 /3 width=7 by drops_after_fwd_drop2, after_isid_isuni/ qed-.
 
 (* Inversion lemmas with uniform relocations ********************************)
@@ -358,7 +358,7 @@ lemma drops_inv_atom2: ∀b,L,f. ⬇*[b, f] L ≘ ⋆ →
 ]
 qed-.
 
-lemma drops_inv_succ: â\88\80L1,L2,i. â¬\87*[⫯i] L1 ≘ L2 →
+lemma drops_inv_succ: â\88\80L1,L2,i. â¬\87*[â\86\91i] L1 ≘ L2 →
                       ∃∃I,K. ⬇*[i] K ≘ L2 & L1 = K.ⓘ{I}.
 #L1 #L2 #i #H elim (drops_inv_isuni … H) -H // *
 [ #H elim (isid_inv_next … H) -H //
@@ -418,11 +418,11 @@ qed-.
 
 lemma drops_tls_at: ∀f,i1,i2. @⦃i1,f⦄ ≘ i2 →
                     ∀b,L1,L2. ⬇*[b,⫱*[i2]f] L1 ≘ L2 →
-                    â¬\87*[b,â\86\91⫱*[⫯i2]f] L1 ≘ L2.
+                    â¬\87*[b,⫯⫱*[â\86\91i2]f] L1 ≘ L2.
 /3 width=3 by drops_eq_repl_fwd, at_inv_tls/ qed-.
 
 lemma drops_split_trans_bind2: ∀b,f,I,L,K0. ⬇*[b, f] L ≘ K0.ⓘ{I} → ∀i. @⦃O, f⦄ ≘ i →
-                               â\88\83â\88\83J,K. â¬\87*[i]L â\89\98 K.â\93\98{J} & â¬\87*[b, ⫱*[⫯i]f] K â\89\98 K0 & â¬\86*[⫱*[⫯i]f] I ≘ J.
+                               â\88\83â\88\83J,K. â¬\87*[i]L â\89\98 K.â\93\98{J} & â¬\87*[b, ⫱*[â\86\91i]f] K â\89\98 K0 & â¬\86*[⫱*[â\86\91i]f] I ≘ J.
 #b #f #I #L #K0 #H #i #Hf
 elim (drops_split_trans … H) -H [ |5: @(after_uni_dx … Hf) |2,3: skip ] /2 width=1 by after_isid_dx/ #Y #HLY #H
 lapply (drops_tls_at … Hf … H) -H #H