lambdadelta

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / cnx.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
index ecc67cb4f9ecd49b47eaffdfc2bd5c11e11d9d9b..8e6dd66ba0d6694f8516150737486fbd9e96fbcd 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/notation/relations/normal_4.ma".
 include "basic_2/reduction/cnr.ma".
 include "basic_2/reduction/cpx.ma".
 
@@ -62,7 +63,7 @@ lemma cnx_inv_zeta: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃+ⓓV.T⦄ → ⊥.
   lapply (H U ?) -H /2 width=3/ #H destruct
   elim (lift_inv_pair_xy_y … HTU)
 | #HT
-  elim (cpss_delift (⋆) V T (⋆. ⓓV) 0 ?) // #T2 #T1 #HT2 #HT12
+  elim (cpr_delift (⋆) V T (⋆.ⓓV) 0) // #T2 #T1 #HT2 #HT12
   lapply (H (+ⓓV.T2) ?) -H /5 width=1/ -HT2 #H destruct /3 width=2/
 ]
 qed-.
@@ -75,7 +76,7 @@ lemma cnx_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃ⓐV.T⦄ →
 | generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H
   [ elim (lift_total V1 0 1) #V2 #HV12
     lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3/ -HV12 #H destruct
-  | lapply (H (ⓓ{a}V1.U1) ?) -H /3 width=1/ #H destruct
+  | lapply (H (ⓓ{a}ⓝW1.V1.U1) ?) -H /3 width=1/ #H destruct
 ]
 qed-.
 
@@ -113,7 +114,7 @@ qed.
 lemma cnx_appl_simple: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃V⦄ → ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → 𝐒⦃T⦄ →
                        ⦃h, L⦄ ⊢ 𝐍[g]⦃ⓐV.T⦄.
 #h #g #L #V #T #HV #HT #HS #X #H
-elim (cpx_inv_appl1_simple … H ?) -H // #V0 #T0 #HV0 #HT0 #H destruct
+elim (cpx_inv_appl1_simple … H) -H // #V0 #T0 #HV0 #HT0 #H destruct
 >(HV … HV0) -V0 >(HT … HT0) -T0 //
 qed.