]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/unfold/tpss_alt.ma
- improved Makefile esp. with the "trim" function
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / unfold / tpss_alt.ma
index 46e064ca9fab22d5549076b3f2b5807d6986a7c4..8f77dd0d0d8e3115a3dd805428e1b1d76ac5ed0e 100644 (file)
@@ -79,7 +79,7 @@ qed.
 
 lemma tpssa_tpss: ∀L,T1,T2,d,e. L ⊢ T1 ▶▶* [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
 #L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e // /2 width=6/
-qed-. 
+qed-.
 
 lemma tpss_ind_alt: ∀R:nat→nat→lenv→relation term.
                     (∀L,I,d,e. R d e L (⓪{I}) (⓪{I})) →