X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fmultiple%2Flifts.ma;h=ff8a0164cc7d9e3b337afe638a4cacba3c39f909;hb=291fe1d3b56faf91d07099f43f3ebde2988649e1;hp=d49e1608d2a6b162e33614431f83852b7e9f456c;hpb=b5507c449ba38a76666a35664f9cf4e1953ad8ec;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts.ma index d49e1608d..ff8a0164c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts.ma @@ -22,7 +22,7 @@ include "basic_2A/substitution/lift.ma". inductive lifts: mr2 → relation term ≝ | lifts_nil : ∀T. lifts (𝐞) T T | lifts_cons: ∀T1,T,T2,cs,l,m. - ⬆[l,m] T1 ≡ T → lifts cs T T2 → lifts (❨l, m❩; cs) T1 T2 + ⬆[l,m] T1 ≡ T → lifts cs T T2 → lifts (❨l, m❩◗ cs) T1 T2 . interpretation "generic relocation (term)" @@ -39,7 +39,7 @@ lemma lifts_inv_nil: ∀T1,T2. ⬆*[𝐞] T1 ≡ T2 → T1 = T2. /2 width=3 by lifts_inv_nil_aux/ qed-. fact lifts_inv_cons_aux: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 → - ∀l,m,tl. cs = ❨l, m❩; tl → + ∀l,m,tl. cs = ❨l, m❩◗ tl → ∃∃T. ⬆[l, m] T1 ≡ T & ⬆*[tl] T ≡ T2. #T1 #T2 #cs * -T1 -T2 -cs [ #T #l #m #tl #H destruct @@ -47,7 +47,7 @@ fact lifts_inv_cons_aux: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 → /2 width=3 by ex2_intro/ qed-. -lemma lifts_inv_cons: ∀T1,T2,l,m,cs. ⬆*[❨l, m❩; cs] T1 ≡ T2 → +lemma lifts_inv_cons: ∀T1,T2,l,m,cs. ⬆*[❨l, m❩◗ cs] T1 ≡ T2 → ∃∃T. ⬆[l, m] T1 ≡ T & ⬆*[cs] T ≡ T2. /2 width=3 by lifts_inv_cons_aux/ qed-.