- lambdadelta: first recursive part of preservation finally proved!

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs.ma
index fded17bd178a09829c96466b7ee7b9f86177df62..5ad9180ac439f950d97e19f7fd845d8fdaec2743 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/lfpcs.ma
@@ -41,9 +41,12 @@ qed-.
 lemma lfpcs_refl: reflexive … lfpcs.
 /2 width=1/ qed.
 
-lemma lfprs_sym: symmetric … lfpcs.
+lemma lfpcs_sym: symmetric … lfpcs.
 /3 width=1/ qed.
 
+lemma lfpc_lfpcs: ∀L1,L2. ⦃L1⦄ ⬌ ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
+/2 width=1/ qed.
+
 lemma lfpcs_strap1: ∀L1,L,L2. ⦃L1⦄ ⬌* ⦃L⦄ → ⦃L⦄ ⬌ ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
 /2 width=3/ qed.