X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Funfold%2Fltpss.ma;h=e992e2a77b63a4ecbf8d301991b16798103931e8;hb=a631aba16617079b3f4cba2ec5a5ef651090e48c;hp=c445f68900fe38b1edacbd089c5118abd9321373;hpb=a8c166f1e1baeeae04553058bd179420ada8bbe7;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma
index c445f6890..e992e2a77 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma
@@ -31,6 +31,12 @@ lemma ltpss_ind: ∀d,e,L1. ∀R:predicate lenv. R L1 →
 #d #e #L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) //
 qed-.
 
+lemma ltpss_ind_dx: ∀d,e,L2. ∀R:predicate lenv. R L2 →
+                    (∀L1,L. L1 [d, e] ▶ L → L [d, e] ▶* L2 → R L → R L1) →
+                    ∀L1. L1 [d, e] ▶* L2 → R L1.
+#d #e #L2 #R #HL2 #IHL2 #L1 #HL12 @(TC_star_ind_dx … HL2 IHL2 … HL12) //
+qed-.
+
 (* Basic properties *********************************************************)
 
 lemma ltpss_strap: ∀L1,L,L2,d,e.