X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fmultiple%2Flifts.ma;h=f83cbdf88944adc56ef255f5d278866da4a57aca;hp=a39b47cbd2ee3ab336b14c7db6188eba616e30fe;hb=2f6f2b7c01d47d23f61dd48d767bcb37aecdcfea;hpb=3a4509b8e569181979f5b15808361c83eb1ae49a

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts.ma
index a39b47cbd..f83cbdf88 100644
--- a/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts.ma
@@ -51,7 +51,6 @@ 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-.
 
-(* Basic_1: was: lift1_sort *)
 lemma lifts_inv_sort1: ∀T2,k,cs. ⬆*[cs] ⋆k ≡ T2 → T2 = ⋆k.
 #T2 #k #cs elim cs -cs
 [ #H <(lifts_inv_nil … H) -H //
@@ -61,7 +60,6 @@ lemma lifts_inv_sort1: ∀T2,k,cs. ⬆*[cs] ⋆k ≡ T2 → T2 = ⋆k.
 ]
 qed-.
 
-(* Basic_1: was: lift1_lref *)
 lemma lifts_inv_lref1: ∀T2,cs,i1. ⬆*[cs] #i1 ≡ T2 →
                        ∃∃i2. @❪i1, cs❫ ≘ i2 & T2 = #i2.
 #T2 #cs elim cs -cs
@@ -82,7 +80,6 @@ lemma lifts_inv_gref1: ∀T2,p,cs. ⬆*[cs] §p ≡ T2 → T2 = §p.
 ]
 qed-.
 
-(* Basic_1: was: lift1_bind *)
 lemma lifts_inv_bind1: ∀a,I,T2,cs,V1,U1. ⬆*[cs] ⓑ{a,I} V1. U1 ≡ T2 →
                        ∃∃V2,U2. ⬆*[cs] V1 ≡ V2 & ⬆*[cs + 1] U1 ≡ U2 &
                                 T2 = ⓑ{a,I} V2. U2.
@@ -97,7 +94,6 @@ lemma lifts_inv_bind1: ∀a,I,T2,cs,V1,U1. ⬆*[cs] ⓑ{a,I} V1. U1 ≡ T2 →
 ]
 qed-.
 
-(* Basic_1: was: lift1_flat *)
 lemma lifts_inv_flat1: ∀I,T2,cs,V1,U1. ⬆*[cs] ⓕ{I} V1. U1 ≡ T2 →
                        ∃∃V2,U2. ⬆*[cs] V1 ≡ V2 & ⬆*[cs] U1 ≡ U2 &
                                 T2 = ⓕ{I} V2. U2.