X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fequivalence%2Flfpcs_lfpcs.ma;h=1e9521736fb711fb300b6f206d27bcce4954a96d;hb=24ccb1f19b64d27f0f3c766e2b1503bd8e3b4786;hp=434068e4fc08e7a8afdc77a70d74ec28c0f5a8c4;hpb=e8998d29ab83e7b6aa495a079193705b2f6743d3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_lfpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_lfpcs.ma
index 434068e4f..1e9521736 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_lfpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs_lfpcs.ma
@@ -44,7 +44,7 @@ theorem lfpcs_trans: ∀L1,L. ⦃L1⦄ ⬌* ⦃L⦄ → ∀L2. ⦃L⦄ ⬌* ⦃L
 /2 width=3/ qed.
 
 theorem lfpcs_canc_sn: ∀L,L1,L2. ⦃L⦄ ⬌* ⦃L1⦄ → ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
-/3 width=3 by lfpcs_trans, lfprs_sym/ qed.
+/3 width=3 by lfpcs_trans, lfpcs_sym/ qed.
 
 theorem lfpcs_canc_dx: ∀L,L1,L2. ⦃L1⦄ ⬌* ⦃L⦄ → ⦃L2⦄ ⬌* ⦃L⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
-/3 width=3 by lfpcs_trans, lfprs_sym/ qed.
+/3 width=3 by lfpcs_trans, lfpcs_sym/ qed.