X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fcomputation%2Fcprs_cprs.ma;h=518c2bd07295a88765cbe26ed0a2785cfaf8971e;hb=e0827239f4b44f2af9c7f88c4c7c41f2a193ae37;hp=ca3fe09da3316f6e9c6066f10f4beb06710cc0d9;hpb=11a20b624a4b5ed18008678cf6cd46dd9a32634d;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma
index ca3fe09da..518c2bd07 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma
@@ -40,6 +40,11 @@ lemma cpr_abbr2: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡ T
 lapply (lcpr_cpr_trans (L. ⓓV1) … HT12) /2 width=1/
 qed.
 
+(* Basic_1: was: pr3_strip *)
+lemma cprs_strip: ∀L,T1,T. L ⊢ T ➡* T1 → ∀T2. L ⊢ T ➡ T2 →
+                  ∃∃T0. L ⊢ T1 ➡ T0 & L ⊢ T2 ➡* T0.
+/3 width=3/ qed.
+
 (* Advanced inversion lemmas ************************************************)
 
 (* Basic_1: was pr3_gen_appl *)