X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fequivalence%2Flfpcs.ma;h=fded17bd178a09829c96466b7ee7b9f86177df62;hb=53f874fba5b9c39a788085515a4fefe5d29281da;hp=c3cbf6c0159e14d2b284fd5662251489ffb6aa75;hpb=7bedf1797ba168f0742194b2add69575e5d4a5cd;p=helm.git

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 c3cbf6c01..fded17bd1 100644
--- 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.