]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_dx.ma
- improved Makefile esp. with the "trim" function
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / ssta_ltpss_dx.ma
index ccc9ecc9d3214a785c419b8c5579aaf54bdef9a5..48ac6a400ca6a753fc8d72abbecaa8d630dd6aea 100644 (file)
@@ -106,7 +106,7 @@ lemma ssta_ltpss_dx_tps_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1
                               ∀L2,d,e. L1 ▶* [d, e] L2 →
                               ∀T2. L2 ⊢ T1 ▶ [d, e] T2 →
                               ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 &
-                                   L2 ⊢ U1 ▶* [d, e] U2.
+                                    L2 ⊢ U1 ▶* [d, e] U2.
 /3 width=5/ qed.
 
 lemma ssta_ltpss_dx_conf: ∀h,g,L1,T,U1,l. ⦃h, L1⦄ ⊢ T •[g, l] U1 →