- improved Makefile esp. with the "trim" function

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_fpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_fpr.ma
index 9dc995fc79e35fa9723ffb1dcd7dc3991acff5a3..f798d566b9d9618847f2e049a8e8ef1f1be69e9b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_fpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_fpr.ma
@@ -22,7 +22,7 @@ include "basic_2/reducibility/cfpr_cpr.ma".
 lemma fpr_lfpr: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1⦄ ➡ ⦃L2⦄.
 #L1 #L2 #T1 #T2 #H
 elim (fpr_inv_all … H) -H /2 width=3/
-qed. 
+qed.
 
 (* Inversion lemmas on context-free parallel reduction for closures *********)