- we introduced the pointer_step rc in the perspective of proving

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

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