- improved Makefile esp. with the "trim" function

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reducibility / tpr.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr.ma
index 957b5f3a89926458ddf3feaa3371b7bc68766e0d..f04b1d9722db49b842220ad6f69d175d60ea7d3f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr.ma
@@ -205,6 +205,15 @@ lemma tpr_inv_lref2: ∀T1,i. T1 ➡ #i →
 
 (* Basic forward lemmas *****************************************************)
 
+lemma tpr_fwd_bind1_minus: ∀I,V1,T1,T. -ⓑ{I}V1.T1 ➡ T → ∀b.
+                           ∃∃V2,T2. ⓑ{b,I}V1.T1 ➡ ⓑ{b,I}V2.T2 &
+                                    T = -ⓑ{I}V2.T2.
+#I #V1 #T1 #T #H #b elim (tpr_inv_bind1 … H) -H *
+[ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct /3 width=4/
+| #T2 #_ #_ #H destruct
+]
+qed-.
+
 lemma tpr_fwd_shift1: ∀L1,T1,T. L1 @@ T1 ➡ T →
                       ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
 #L1 @(lenv_ind_dx … L1) -L1 normalize
@@ -225,5 +234,5 @@ qed-.
 
 (* Basic_1: removed theorems 3:
             pr0_subst0_back pr0_subst0_fwd pr0_subst0
-   Basic_1: removed local theorems: 1: pr0_delta_tau
 *)
+(* Basic_1: removed local theorems: 1: pr0_delta_tau *)