X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fequivalence%2Fcpcs_cpcs.ma;h=fcad182e0a2d88d63133ee160fab9fceee530fa1;hb=fec1a061eeca5e7e05b4f0c3e299983b163569c3;hp=d67e6663004cd4268b185d7831a3e4ffad502659;hpb=69644bb333b2862a5ff2ff434df8830e854e3385;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma
index d67e66630..fcad182e0 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma
@@ -73,6 +73,10 @@ elim (cprs_inv_abst1 Abst W1 … H1) -H1 #W2 #T2 #HW12 #HT12 #H destruct
 @(ex2_2_intro … H2) -H2 /2 width=2/ (**) (* explicit constructor, /3 width=6/ is slow *)
 qed-.
 
+lemma cpcs_inv_abst2: ∀L,W1,T1,T. L ⊢ T ⬌* ⓛW1.T1 →
+                      ∃∃W2,T2. L ⊢ T ➡* ⓛW2.T2 & L ⊢ ⓛW1.T1 ➡* ⓛW2.T2.
+/3 width=1 by cpcs_inv_abst1, cpcs_sym/ qed-.
+
 (* Basic_1: was: pc3_gen_lift *)
 lemma cpcs_inv_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K →
                      ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ U2 →