- we set up the support for the "bt-reduction" of Automath literature

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / unfold / lifts.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma
index 6a3c647a0cfa2b10674332c5fdd78f84fb52c192..40158acbe45749e94d83aa002831ccffa248acc4 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma
@@ -12,15 +12,15 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Basic_2/substitution/lift.ma".
-include "Basic_2/unfold/gr2_plus.ma".
+include "basic_2/substitution/lift.ma".
+include "basic_2/unfold/gr2_plus.ma".
 
 (* GENERIC TERM RELOCATION **************************************************)
 
 inductive lifts: list2 nat nat → relation term ≝
 | 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
+              ⇧[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} @ des) T1 T2
 .
 
 interpretation "generic relocation (term)"
@@ -37,7 +37,7 @@ lemma lifts_inv_nil: ∀T1,T2. ⇧*[⟠] T1 ≡ T2 → T1 = T2.
 /2 width=3/ qed-.
 
 fact lifts_inv_cons_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 →
-                         ∀d,e,tl. des = {d, e} :: tl →
+                         ∀d,e,tl. des = {d, e} @ tl →
                          ∃∃T. ⇧[d, e] T1 ≡ T & ⇧*[tl] T ≡ T2.
 #T1 #T2 #des * -T1 -T2 -des
 [ #T #d #e #tl #H destruct
@@ -45,7 +45,7 @@ fact lifts_inv_cons_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 →
   /2 width=3/
 qed.
 
-lemma lifts_inv_cons: ∀T1,T2,d,e,des. ⇧*[{d, e} :: des] T1 ≡ T2 →
+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-.
 
@@ -61,7 +61,7 @@ qed-.
 
 (* Basic_1: was: lift1_lref *)
 lemma lifts_inv_lref1: ∀T2,des,i1. ⇧*[des] #i1 ≡ T2 →
-                       ∃∃i2. @[i1] des ≡ i2 & T2 = #i2.
+                       ∃∃i2. @⦃i1, des⦄ ≡ i2 & T2 = #i2.
 #T2 #des elim des -des
 [ #i1 #H <(lifts_inv_nil … H) -H /2 width=3/
 | #d #e #des #IH #i1 #H
@@ -81,10 +81,10 @@ lemma lifts_inv_gref1: ∀T2,p,des. ⇧*[des] §p ≡ T2 → T2 = §p.
 qed-.
 
 (* Basic_1: was: lift1_bind *)
-lemma lifts_inv_bind1: ∀I,T2,des,V1,U1. ⇧*[des] ⓑ{I} V1. U1 ≡ T2 →
+lemma lifts_inv_bind1: ∀a,I,T2,des,V1,U1. ⇧*[des] ⓑ{a,I} V1. U1 ≡ T2 →
                        ∃∃V2,U2. ⇧*[des] V1 ≡ V2 & ⇧*[des + 1] U1 ≡ U2 &
-                                T2 = ⓑ{I} V2. U2.
-#I #T2 #des elim des -des
+                                T2 = ⓑ{a,I} V2. U2.
+#a #I #T2 #des elim des -des
 [ #V1 #U1 #H
   <(lifts_inv_nil … H) -H /2 width=5/
 | #d #e #des #IHdes #V1 #U1 #H
@@ -112,20 +112,20 @@ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma lifts_simple_dx: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒[T1] → 𝐒[T2].
+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/
 qed-.
 
-lemma lifts_simple_sn: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒[T2] → 𝐒[T1].
+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/
 qed-.
 
 (* Basic properties *********************************************************)
 
-lemma lifts_bind: ∀I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 →
+lemma lifts_bind: ∀a,I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 →
                   ∀T1. ⇧*[des + 1] T1 ≡ T2 →
-                  ⇧*[des] ⓑ{I} V1. T1 ≡ ⓑ{I} V2. T2.
-#I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
+                  ⇧*[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
   elim (lifts_inv_cons … H) -H /3 width=3/