X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Flifts.ma;h=31b383145b7e744f1d5ba1b9c8168a919c2cf9d5;hb=50001ac0b45a3f6376e8cbfd9200149a01d68148;hp=20727c4cdb8434f65a8090baef6612dddf62e078;hpb=c559209567ff7ec5e4d3de7fef431398f9ba2559;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts.ma
index 20727c4cd..31b383145 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts.ma
@@ -19,7 +19,7 @@ include "basic_2/substitution/gr2_plus.ma".
 (* GENERIC TERM RELOCATION **************************************************)
 
 inductive lifts: list2 nat nat → relation term ≝
-| lifts_nil : ∀T. lifts ⟠ T T
+| lifts_nil : ∀T. lifts (⟠) T T
 | lifts_cons: ∀T1,T,T2,des,d,e.
               ⇧[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} @ des) T1 T2
 .
@@ -32,10 +32,10 @@ interpretation "generic relocation (term)"
 fact lifts_inv_nil_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → des = ⟠ → T1 = T2.
 #T1 #T2 #des * -T1 -T2 -des //
 #T1 #T #T2 #d #e #des #_ #_ #H destruct
-qed.
+qed-.
 
 lemma lifts_inv_nil: ∀T1,T2. ⇧*[⟠] T1 ≡ T2 → T1 = T2.
-/2 width=3/ qed-.
+/2 width=3 by lifts_inv_nil_aux/ qed-.
 
 fact lifts_inv_cons_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 →
                          ∀d,e,tl. des = {d, e} @ tl →
@@ -43,12 +43,12 @@ fact lifts_inv_cons_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ 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/
-qed.
+  /2 width=3 by ex2_intro/
+qed-.
 
 lemma lifts_inv_cons: ∀T1,T2,d,e,des. ⇧*[{d, e} @ des] T1 ≡ T2 →
                       ∃∃T. ⇧[d, e] T1 ≡ T & ⇧*[des] T ≡ T2.
-/2 width=3/ qed-.
+/2 width=3 by lifts_inv_cons_aux/ qed-.
 
 (* Basic_1: was: lift1_sort *)
 lemma lifts_inv_sort1: ∀T2,k,des. ⇧*[des] ⋆k ≡ T2 → T2 = ⋆k.
@@ -56,7 +56,7 @@ lemma lifts_inv_sort1: ∀T2,k,des. ⇧*[des] ⋆k ≡ T2 → T2 = ⋆k.
 [ #H <(lifts_inv_nil … H) -H //
 | #d #e #des #IH #H
   elim (lifts_inv_cons … H) -H #X #H
-  >(lift_inv_sort1 … H) -H /2 width=1/
+  >(lift_inv_sort1 … H) -H /2 width=1 by/
 ]
 qed-.
 
@@ -64,11 +64,11 @@ qed-.
 lemma lifts_inv_lref1: ∀T2,des,i1. ⇧*[des] #i1 ≡ T2 →
                        ∃∃i2. @⦃i1, des⦄ ≡ i2 & T2 = #i2.
 #T2 #des elim des -des
-[ #i1 #H <(lifts_inv_nil … H) -H /2 width=3/
+[ #i1 #H <(lifts_inv_nil … H) -H /2 width=3 by at_nil, ex2_intro/
 | #d #e #des #IH #i1 #H
   elim (lifts_inv_cons … H) -H #X #H1 #H2
   elim (lift_inv_lref1 … H1) -H1 * #Hdi1 #H destruct
-  elim (IH … H2) -IH -H2 /3 width=3/
+  elim (IH … H2) -IH -H2 /3 width=3 by at_lt, at_ge, ex2_intro/
 ]
 qed-.
 
@@ -77,7 +77,7 @@ lemma lifts_inv_gref1: ∀T2,p,des. ⇧*[des] §p ≡ T2 → T2 = §p.
 [ #H <(lifts_inv_nil … H) -H //
 | #d #e #des #IH #H
   elim (lifts_inv_cons … H) -H #X #H
-  >(lift_inv_gref1 … H) -H /2 width=1/
+  >(lift_inv_gref1 … H) -H /2 width=1 by/
 ]
 qed-.
 
@@ -87,12 +87,12 @@ lemma lifts_inv_bind1: ∀a,I,T2,des,V1,U1. ⇧*[des] ⓑ{a,I} V1. U1 ≡ T2 →
                                 T2 = ⓑ{a,I} V2. U2.
 #a #I #T2 #des elim des -des
 [ #V1 #U1 #H
-  <(lifts_inv_nil … H) -H /2 width=5/
+  <(lifts_inv_nil … H) -H /2 width=5 by ex3_2_intro, lifts_nil/
 | #d #e #des #IHdes #V1 #U1 #H
   elim (lifts_inv_cons … H) -H #X #H #HT2
   elim (lift_inv_bind1 … H) -H #V #U #HV1 #HU1 #H destruct
   elim (IHdes … HT2) -IHdes -HT2 #V2 #U2 #HV2 #HU2 #H destruct
-  /3 width=5/
+  /3 width=5 by ex3_2_intro, lifts_cons/
 ]
 qed-.
 
@@ -102,23 +102,23 @@ lemma lifts_inv_flat1: ∀I,T2,des,V1,U1. ⇧*[des] ⓕ{I} V1. U1 ≡ T2 →
                                 T2 = ⓕ{I} V2. U2.
 #I #T2 #des elim des -des
 [ #V1 #U1 #H
-  <(lifts_inv_nil … H) -H /2 width=5/
+  <(lifts_inv_nil … H) -H /2 width=5 by ex3_2_intro, lifts_nil/
 | #d #e #des #IHdes #V1 #U1 #H
   elim (lifts_inv_cons … H) -H #X #H #HT2
   elim (lift_inv_flat1 … H) -H #V #U #HV1 #HU1 #H destruct
   elim (IHdes … HT2) -IHdes -HT2 #V2 #U2 #HV2 #HU2 #H destruct
-  /3 width=5/
+  /3 width=5 by ex3_2_intro, lifts_cons/
 ]
 qed-.
 
 (* Basic forward lemmas *****************************************************)
 
 lemma lifts_simple_dx: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
-#T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_dx/
+#T1 #T2 #des #H elim H -T1 -T2 -des /3 width=5 by lift_simple_dx/
 qed-.
 
 lemma lifts_simple_sn: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
-#T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_sn/
+#T1 #T2 #des #H elim H -T1 -T2 -des /3 width=5 by lift_simple_sn/
 qed-.
 
 (* Basic properties *********************************************************)
@@ -129,7 +129,7 @@ lemma lifts_bind: ∀a,I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 →
 #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
-  elim (lifts_inv_cons … H) -H /3 width=3/
+  elim (lifts_inv_cons … H) -H /3 width=3 by lift_bind, lifts_cons/
 ]
 qed.
 
@@ -139,13 +139,12 @@ lemma lifts_flat: ∀I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 →
 #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
-  elim (lifts_inv_cons … H) -H /3 width=3/
+  elim (lifts_inv_cons … H) -H /3 width=3 by lift_flat, lifts_cons/
 ]
 qed.
 
 lemma lifts_total: ∀des,T1. ∃T2. ⇧*[des] T1 ≡ T2.
-#des elim des -des /2 width=2/
-#d #e #des #IH #T1
-elim (lift_total T1 d e) #T #HT1
-elim (IH T) -IH /3 width=4/
+#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/
 qed.