uncommited file found :)

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / unwind / sstas_ltpss_dx.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_dx.ma
index 84f2d805bef1f239e29ab757102f12b630a658c6..2a8f8e7d283e566d7684a109d6fc5080f755dbea 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_dx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_ltpss_dx.ma
@@ -24,20 +24,17 @@ lemma sstas_ltpss_dx_tpss_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 
                                 ∀T2. L2 ⊢ T1 ▶* [d, e] T2 →
                                 ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 &
                                       L2 ⊢ U1 ▶* [d, e] U2.
-#h #g #L1 #T1 #U1 #H @(sstas_ind_alt … H) -T1
-[ #T1 #l #HUT1 #L2 #d #e #HL12 #U2 #HU12
-  elim (ssta_ltpss_dx_tpss_conf … HUT1 … HL12 … HU12) -HUT1 -HL12 /3 width=3/
-| #T0 #U0 #l0 #HTU0 #_ #IHU01 #L2 #d #e #HL12 #T #HT0
-  elim (ssta_ltpss_dx_tpss_conf … HTU0 … HL12 … HT0) -HTU0 -HT0 #U #HTU #HU0
-  elim (IHU01 … HL12 … HU0) -IHU01 -HL12 -U0 /3 width=4/
-]
+#h #g #L1 #T1 #U1 #H @(sstas_ind_dx … H) -T1 /2 width=3/
+#T0 #U0 #l0 #HTU0 #_ #IHU01 #L2 #d #e #HL12 #T #HT0
+elim (ssta_ltpss_dx_tpss_conf … HTU0 … HL12 … HT0) -HTU0 -HT0 #U #HTU #HU0
+elim (IHU01 … HL12 … HU0) -IHU01 -HL12 -U0 /3 width=4/
 qed.
 
 lemma sstas_ltpss_dx_tps_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 →
                                ∀L2,d,e. L1 ▶* [d, e] L2 →
                                ∀T2. L2 ⊢ T1 ▶ [d, e] T2 →
                                ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 & L2 ⊢ U1 ▶* [d, e] U2.
-/3 width=5/ qed.
+/3 width=7 by step, sstas_ltpss_dx_tpss_conf/ qed. (**) (* auto fails without trace *)
 
 lemma sstas_ltpss_dx_conf: ∀h,g,L1,T,U1. ⦃h, L1⦄ ⊢ T •*[g] U1 →
                            ∀L2,d,e. L1 ▶* [d, e] L2 →