- we polarized binders to control zeta reduction

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / computation / cprs_lcprs.ma

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 5efdb4fa2027fbfc11660a80a5385d538db40a30..9131ba4c27de4f5f57df3c3475ba1f07ee0c413e 100644 (file)
--- 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 *