- lambdadelta: more service lemmas ...

[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 9a226be58ddf8b85fca73971a05d4e1b97935987..9dc995fc79e35fa9723ffb1dcd7dc3991acff5a3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_fpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_fpr.ma
@@ -17,7 +17,7 @@ include "basic_2/reducibility/cfpr_cpr.ma".
 
 (* FOCALIZED PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ***********************)
 
-(* Inversion lemmas on context-free parallel reduction for closures *********)
+(* Properties on context-free parallel reduction for closures ***************)
 
 lemma fpr_lfpr: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1⦄ ➡ ⦃L2⦄.
 #L1 #L2 #T1 #T2 #H