X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fcomputation%2Fcprs_lcprs.ma;h=9131ba4c27de4f5f57df3c3475ba1f07ee0c413e;hb=a2144f09d1bd7022c1f2dfd4909a1fb9772c8d56;hp=5efdb4fa2027fbfc11660a80a5385d538db40a30;hpb=770ba48ba232d7f1782629c572820a0f1bfe4fde;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcprs.ma
index 5efdb4fa2..9131ba4c2 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcprs.ma
@@ -32,12 +32,12 @@ lemma lcprs_cpr_trans: ∀L1,L2. L1 ⊢ ➡* L2 →
 (* Advanced inversion lemmas ************************************************)
 
 (* Basic_1: was pr3_gen_abbr *)
-lemma cprs_inv_abbr1: ∀L,V1,T1,U2. L ⊢ ⓓV1. T1 ➡* U2 →
+lemma cprs_inv_abbr1: ∀a,L,V1,T1,U2. L ⊢ ⓓ{a}V1. T1 ➡* U2 →
                       (∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓓV1 ⊢ T1 ➡* T2 &
-                                U2 = ⓓV2. T2
+                                U2 = ⓓ{a}V2. T2
                       ) ∨
-                      ∃∃T2. L. ⓓV1 ⊢ T1 ➡* T2 & ⇧[0, 1] U2 ≡ T2.
-#L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
+                      ∃∃T2. L. ⓓV1 ⊢ T1 ➡* T2 & ⇧[0, 1] U2 ≡ T2 & a = true.
+#a #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
 #U0 #U2 #_ #HU02 * *
 [ #V0 #T0 #HV10 #HT10 #H destruct
   elim (cpr_inv_abbr1 … HU02) -HU02 *