partial commit in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / equivalence / lfpcs_lfpcs.ma

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 434068e4fc08e7a8afdc77a70d74ec28c0f5a8c4..1e9521736fb711fb300b6f206d27bcce4954a96d 100644 (file)
--- 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.