X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Fcpg_drops.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Fcpg_drops.ma;h=758a278b7a15645529c1997f15f239e8104c1155;hb=6555775aa5268dec0d9ae4579412b659cacdc964;hp=6c9fdfd22190e36447009acb8ebb9abfd6e4b55c;hpb=69592aa1d0c0d122fb09f11cc53bf4c5a1532fdd;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma
index 6c9fdfd22..758a278b7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma
@@ -81,7 +81,7 @@ qed-.
 (* Properties with generic slicing for local environments *******************)
 
 (* Note: it should use drops_split_trans_pair2 *)
-lemma cpg_lifts: ∀Rt. reflexive … Rt → ∀c,h,G. d_liftable2 (cpg Rt h c G).
+lemma cpg_lifts_sn: ∀Rt. reflexive … Rt → ∀c,h,G. d_liftable2_sn (cpg Rt h c G).
 #Rt #HRt #c #h #G #K #T generalize in match c; -c
 @(fqup_wf_ind_eq … G K T) -G -K -T #G0 #K0 #T0 #IH #G #K * *
 [ #s #HG #HK #HT #c #X2 #H2 #b #f #L #HLK #X1 #H1 destruct -IH
@@ -158,9 +158,12 @@ lemma cpg_lifts: ∀Rt. reflexive … Rt → ∀c,h,G. d_liftable2 (cpg Rt h c G
 ]
 qed-.
 
+lemma cpg_lifts_bi: ∀Rt. reflexive … Rt → ∀c,h,G. d_liftable2_bi (cpg Rt h c G).
+/3 width=9 by cpg_lifts_sn, d_liftable2_sn_bi/ qed-.
+
 (* Inversion lemmas with generic slicing for local environments *************)
 
-lemma cpg_inv_lifts1: ∀Rt. reflexive … Rt → ∀c,h,G. d_deliftable2_sn (cpg Rt h c G).
+lemma cpg_inv_lifts_sn: ∀Rt. reflexive … Rt → ∀c,h,G. d_deliftable2_sn (cpg Rt h c G).
 #Rt #HRt #c #h #G #L #U generalize in match c; -c
 @(fqup_wf_ind_eq … G L U) -G -L -U #G0 #L0 #U0 #IH #G #L * *
 [ #s #HG #HL #HU #c #X2 #H2 #b #f #K #HLK #X1 #H1 destruct -IH
@@ -232,3 +235,6 @@ lemma cpg_inv_lifts1: ∀Rt. reflexive … Rt → ∀c,h,G. d_deliftable2_sn (cp
   ]
 ]
 qed-.
+
+lemma cpg_inv_lifts_bi: ∀Rt. reflexive … Rt → ∀c,h,G. d_deliftable2_bi (cpg Rt h c G).
+/3 width=9 by cpg_inv_lifts_sn, d_deliftable2_sn_bi/ qed-.