X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freducibility%2Flfpr_fpr.ma;h=f798d566b9d9618847f2e049a8e8ef1f1be69e9b;hb=08cb57944c0df08611d4f35d286e46c0d13e4813;hp=9dc995fc79e35fa9723ffb1dcd7dc3991acff5a3;hpb=9245402674a791dfdb943902f8288d742088c854;p=helm.git

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 9dc995fc7..f798d566b 100644
--- 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 *********)