X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freducibility%2Fcpr.ma;h=ae8e01bbc027503d67d5fcad7b851b519e981eef;hb=06fae7628917399b6ceabace25607d6aafab0040;hp=fffaad09885f4efc87d7786831839ed4ec902f83;hpb=bdff98417627c404aacec8ebb07812287783c500;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma
index fffaad098..ae8e01bbc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma
@@ -88,6 +88,14 @@ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
+lemma cpr_fwd_bind1_minus: ∀I,L,V1,T1,T. L ⊢ -ⓑ{I}V1.T1 ➡ T → ∀b.
+                           ∃∃V2,T2. L ⊢ ⓑ{b,I}V1.T1 ➡ ⓑ{b,I}V2.T2 &
+                                    T = -ⓑ{I}V2.T2.
+#I #L #V1 #T1 #T * #X #H1 #H2 #b
+elim (tpr_fwd_bind1_minus … H1 b) -H1 #V0 #T0 #HT10 #H destruct
+elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/
+qed-.
+
 lemma cpr_fwd_shift1: ∀L,L1,T1,T. L ⊢ L1 @@ T1 ➡ T →
                       ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
 #L #L1 #T1 #T * #X #H1 #H2