X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fequivalence%2Flfpcs_lfpcs.ma;h=434068e4fc08e7a8afdc77a70d74ec28c0f5a8c4;hb=4bea40e6589ce21c15ecf99bdd5bd2a1c62f6809;hp=fcbeb9b8aad8d117906db727f2c0ac358a261bcd;hpb=7bedf1797ba168f0742194b2add69575e5d4a5cd;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfpcs.ma
index fcbeb9b8a..434068e4f 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfpcs.ma
+++ b/matita/matita/contribs/lambda_delta/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_comm/ qed.
+/3 width=3 by lfpcs_trans, lfprs_sym/ qed.
 
 theorem lfpcs_canc_dx: ∀L,L1,L2. ⦃L1⦄ ⬌* ⦃L⦄ → ⦃L2⦄ ⬌* ⦃L⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
-/3 width=3 by lfpcs_trans, lfprs_comm/ qed.
+/3 width=3 by lfpcs_trans, lfprs_sym/ qed.