- lambdadelta: first recursive part of preservation finally proved!

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma
index a979b7baeab51931bd81076dbd9c6e8b2dbf8f51..8b2259daca1cfad13b07a65019b6bd5cfe3f5b59 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma
@@ -47,6 +47,9 @@ lemma cpcs_refl: ∀L. reflexive … (cpcs L).
 lemma cpcs_sym: ∀L. symmetric … (cpcs L).
 /3 width=1/ qed.
 
+lemma cpc_cpcs: ∀L,T1,T2. L ⊢ T1 ⬌ T2 → L ⊢ T2 ⬌* T2.
+/2 width=1/ qed.
+
 lemma cpcs_strap1: ∀L,T1,T,T2. L ⊢ T1 ⬌* T → L ⊢ T ⬌ T2 → L ⊢ T1 ⬌* T2.
 /2 width=3/ qed.