- lambdadelta: first recursive part of preservation finally proved!

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs.ma
index c0e02359b6ade21a5e95953645162750330ab3b5..45be267815b5cab092bd703ad60af0568c42a1ce 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs.ma
@@ -41,6 +41,9 @@ lemma fpcs_refl: bi_reflexive … fpcs.
 lemma fpcs_sym: bi_symmetric … fpcs.
 /3 width=1/ qed.
 
+lemma fpc_fpcs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⬌ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄.
+/2 width=1/ qed.
+
 lemma fpcs_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ → ⦃L, T⦄ ⬌ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄.
 /2 width=4/ qed.