X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fequivalence%2Ffpcs.ma;h=45be267815b5cab092bd703ad60af0568c42a1ce;hb=514f515ecb8765c68720e880460c2457898d74dc;hp=c0e02359b6ade21a5e95953645162750330ab3b5;hpb=e8998d29ab83e7b6aa495a079193705b2f6743d3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/fpcs.ma
index c0e02359b..45be26781 100644
--- 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.