- we introduced the pointer_step rc in the perspective of proving

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

diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs.ma
index c3cbf6c0159e14d2b284fd5662251489ffb6aa75..fded17bd178a09829c96466b7ee7b9f86177df62 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs.ma
@@ -38,9 +38,12 @@ qed-.
 
 (* Basic properties *********************************************************)
 
-lemma lfpcs_refl: ∀L. ⦃L⦄ ⬌* ⦃L⦄.
+lemma lfpcs_refl: reflexive … lfpcs.
 /2 width=1/ qed.
 
+lemma lfprs_sym: symmetric … lfpcs.
+/3 width=1/ qed.
+
 lemma lfpcs_strap1: ∀L1,L,L2. ⦃L1⦄ ⬌* ⦃L⦄ → ⦃L⦄ ⬌ ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
 /2 width=3/ qed.
 
@@ -64,7 +67,3 @@ lemma lfpcs_lfpr_div: ∀L1,L. ⦃L1⦄ ⬌* ⦃L⦄ → ∀L2. ⦃L2⦄ ➡ ⦃
 
 lemma lfpcs_lfpr_conf: ∀L1,L. ⦃L⦄ ➡ ⦃L1⦄ → ∀L2. ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
 /3 width=3/ qed.
-
-lemma lfprs_comm: ∀L1,L2. ⦃L1⦄ ⬌* ⦃L2⦄ → ⦃L2⦄ ⬌* ⦃L1⦄.
-#L1 #L2 #H @(lfpcs_ind … H) -L2 // /3 width=3/
-qed.