notational change of lift, drop, and gget

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / multiple / lifts.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma
index 2721052555bdc6c63b8f7715e041fe6d670ebde3..8d3d9ccd510a9ba5491c07417739e8b2728a0187 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma
@@ -21,7 +21,7 @@ include "basic_2/multiple/mr2_plus.ma".
 inductive lifts: list2 nat nat → relation term ≝
 | lifts_nil : ∀T. lifts (◊) T T
 | lifts_cons: ∀T1,T,T2,des,d,e.
-              â\87§[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} @ des) T1 T2
+              â¬\86[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} @ des) T1 T2
 .
 
 interpretation "generic relocation (term)"
@@ -29,29 +29,29 @@ interpretation "generic relocation (term)"
 
 (* Basic inversion lemmas ***************************************************)
 
-fact lifts_inv_nil_aux: â\88\80T1,T2,des. â\87§*[des] T1 ≡ T2 → des = ◊ → T1 = T2.
+fact lifts_inv_nil_aux: â\88\80T1,T2,des. â¬\86*[des] T1 ≡ T2 → des = ◊ → T1 = T2.
 #T1 #T2 #des * -T1 -T2 -des //
 #T1 #T #T2 #d #e #des #_ #_ #H destruct
 qed-.
 
-lemma lifts_inv_nil: â\88\80T1,T2. â\87§*[◊] T1 ≡ T2 → T1 = T2.
+lemma lifts_inv_nil: â\88\80T1,T2. â¬\86*[◊] T1 ≡ T2 → T1 = T2.
 /2 width=3 by lifts_inv_nil_aux/ qed-.
 
-fact lifts_inv_cons_aux: â\88\80T1,T2,des. â\87§*[des] T1 ≡ T2 →
+fact lifts_inv_cons_aux: â\88\80T1,T2,des. â¬\86*[des] T1 ≡ T2 →
                          ∀d,e,tl. des = {d, e} @ tl →
-                         â\88\83â\88\83T. â\87§[d, e] T1 â\89¡ T & â\87§*[tl] T ≡ T2.
+                         â\88\83â\88\83T. â¬\86[d, e] T1 â\89¡ T & â¬\86*[tl] T ≡ T2.
 #T1 #T2 #des * -T1 -T2 -des
 [ #T #d #e #tl #H destruct
 | #T1 #T #T2 #des #d #e #HT1 #HT2 #hd #he #tl #H destruct
   /2 width=3 by ex2_intro/
 qed-.
 
-lemma lifts_inv_cons: â\88\80T1,T2,d,e,des. â\87§*[{d, e} @ des] T1 ≡ T2 →
-                      â\88\83â\88\83T. â\87§[d, e] T1 â\89¡ T & â\87§*[des] T ≡ T2.
+lemma lifts_inv_cons: â\88\80T1,T2,d,e,des. â¬\86*[{d, e} @ des] T1 ≡ T2 →
+                      â\88\83â\88\83T. â¬\86[d, e] T1 â\89¡ T & â¬\86*[des] T ≡ T2.
 /2 width=3 by lifts_inv_cons_aux/ qed-.
 
 (* Basic_1: was: lift1_sort *)
-lemma lifts_inv_sort1: â\88\80T2,k,des. â\87§*[des] ⋆k ≡ T2 → T2 = ⋆k.
+lemma lifts_inv_sort1: â\88\80T2,k,des. â¬\86*[des] ⋆k ≡ T2 → T2 = ⋆k.
 #T2 #k #des elim des -des
 [ #H <(lifts_inv_nil … H) -H //
 | #d #e #des #IH #H
@@ -61,7 +61,7 @@ lemma lifts_inv_sort1: ∀T2,k,des. ⇧*[des] ⋆k ≡ T2 → T2 = ⋆k.
 qed-.
 
 (* Basic_1: was: lift1_lref *)
-lemma lifts_inv_lref1: â\88\80T2,des,i1. â\87§*[des] #i1 ≡ T2 →
+lemma lifts_inv_lref1: â\88\80T2,des,i1. â¬\86*[des] #i1 ≡ T2 →
                        ∃∃i2. @⦃i1, des⦄ ≡ i2 & T2 = #i2.
 #T2 #des elim des -des
 [ #i1 #H <(lifts_inv_nil … H) -H /2 width=3 by at_nil, ex2_intro/
@@ -72,7 +72,7 @@ lemma lifts_inv_lref1: ∀T2,des,i1. ⇧*[des] #i1 ≡ T2 →
 ]
 qed-.
 
-lemma lifts_inv_gref1: â\88\80T2,p,des. â\87§*[des] §p ≡ T2 → T2 = §p.
+lemma lifts_inv_gref1: â\88\80T2,p,des. â¬\86*[des] §p ≡ T2 → T2 = §p.
 #T2 #p #des elim des -des
 [ #H <(lifts_inv_nil … H) -H //
 | #d #e #des #IH #H
@@ -82,8 +82,8 @@ lemma lifts_inv_gref1: ∀T2,p,des. ⇧*[des] §p ≡ T2 → T2 = §p.
 qed-.
 
 (* Basic_1: was: lift1_bind *)
-lemma lifts_inv_bind1: â\88\80a,I,T2,des,V1,U1. â\87§*[des] ⓑ{a,I} V1. U1 ≡ T2 →
-                       â\88\83â\88\83V2,U2. â\87§*[des] V1 â\89¡ V2 & â\87§*[des + 1] U1 ≡ U2 &
+lemma lifts_inv_bind1: â\88\80a,I,T2,des,V1,U1. â¬\86*[des] ⓑ{a,I} V1. U1 ≡ T2 →
+                       â\88\83â\88\83V2,U2. â¬\86*[des] V1 â\89¡ V2 & â¬\86*[des + 1] U1 ≡ U2 &
                                 T2 = ⓑ{a,I} V2. U2.
 #a #I #T2 #des elim des -des
 [ #V1 #U1 #H
@@ -97,8 +97,8 @@ lemma lifts_inv_bind1: ∀a,I,T2,des,V1,U1. ⇧*[des] ⓑ{a,I} V1. U1 ≡ T2 →
 qed-.
 
 (* Basic_1: was: lift1_flat *)
-lemma lifts_inv_flat1: â\88\80I,T2,des,V1,U1. â\87§*[des] ⓕ{I} V1. U1 ≡ T2 →
-                       â\88\83â\88\83V2,U2. â\87§*[des] V1 â\89¡ V2 & â\87§*[des] U1 ≡ U2 &
+lemma lifts_inv_flat1: â\88\80I,T2,des,V1,U1. â¬\86*[des] ⓕ{I} V1. U1 ≡ T2 →
+                       â\88\83â\88\83V2,U2. â¬\86*[des] V1 â\89¡ V2 & â¬\86*[des] U1 ≡ U2 &
                                 T2 = ⓕ{I} V2. U2.
 #I #T2 #des elim des -des
 [ #V1 #U1 #H
@@ -113,19 +113,19 @@ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma lifts_simple_dx: â\88\80T1,T2,des. â\87§*[des] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
+lemma lifts_simple_dx: â\88\80T1,T2,des. â¬\86*[des] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
 #T1 #T2 #des #H elim H -T1 -T2 -des /3 width=5 by lift_simple_dx/
 qed-.
 
-lemma lifts_simple_sn: â\88\80T1,T2,des. â\87§*[des] T1 ≡ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
+lemma lifts_simple_sn: â\88\80T1,T2,des. â¬\86*[des] T1 ≡ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
 #T1 #T2 #des #H elim H -T1 -T2 -des /3 width=5 by lift_simple_sn/
 qed-.
 
 (* Basic properties *********************************************************)
 
-lemma lifts_bind: â\88\80a,I,T2,V1,V2,des. â\87§*[des] V1 ≡ V2 →
-                  â\88\80T1. â\87§*[des + 1] T1 ≡ T2 →
-                  â\87§*[des] ⓑ{a,I} V1. T1 ≡ ⓑ{a,I} V2. T2.
+lemma lifts_bind: â\88\80a,I,T2,V1,V2,des. â¬\86*[des] V1 ≡ V2 →
+                  â\88\80T1. â¬\86*[des + 1] T1 ≡ T2 →
+                  â¬\86*[des] ⓑ{a,I} V1. T1 ≡ ⓑ{a,I} V2. T2.
 #a #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
 [ #V #T1 #H >(lifts_inv_nil … H) -H //
 | #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H
@@ -133,9 +133,9 @@ lemma lifts_bind: ∀a,I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 →
 ]
 qed.
 
-lemma lifts_flat: â\88\80I,T2,V1,V2,des. â\87§*[des] V1 ≡ V2 →
-                  â\88\80T1. â\87§*[des] T1 ≡ T2 →
-                  â\87§*[des] ⓕ{I} V1. T1 ≡ ⓕ{I} V2. T2.
+lemma lifts_flat: â\88\80I,T2,V1,V2,des. â¬\86*[des] V1 ≡ V2 →
+                  â\88\80T1. â¬\86*[des] T1 ≡ T2 →
+                  â¬\86*[des] ⓕ{I} V1. T1 ≡ ⓕ{I} V2. T2.
 #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
 [ #V #T1 #H >(lifts_inv_nil … H) -H //
 | #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H
@@ -143,7 +143,7 @@ lemma lifts_flat: ∀I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 →
 ]
 qed.
 
-lemma lifts_total: â\88\80des,T1. â\88\83T2. â\87§*[des] T1 ≡ T2.
+lemma lifts_total: â\88\80des,T1. â\88\83T2. â¬\86*[des] T1 ≡ T2.
 #des elim des -des /2 width=2 by lifts_nil, ex_intro/
 #d #e #des #IH #T1 elim (lift_total T1 d e)
 #T #HT1 elim (IH T) -IH /3 width=4 by lifts_cons, ex_intro/