- commit of the "reduction" component with two additions ...

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma
index c1a44b729dd048041456a1e3fe2d9e4fa0700a1d..34d95faaeed1a272d803e89a44fa588495002186 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma
@@ -25,52 +25,53 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma cnr_inv_delta: ∀G,L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → ⦃G, L⦄ ⊢ 𝐍⦃#i⦄ → ⊥.
+lemma cnr_inv_delta: ∀G,L,K,V,i. ⇩[i] L ≡ K.ⓓV → ⦃G, L⦄ ⊢ 𝐍⦃#i⦄ → ⊥.
 #G #L #K #V #i #HLK #H
 elim (lift_total V 0 (i+1)) #W #HVW
-lapply (H W ?) -H [ /3 width=6/ ] -HLK #H destruct
+lapply (H W ?) -H [ /3 width=6 by cpr_delta/ ] -HLK #H destruct
 elim (lift_inv_lref2_be … HVW) -HVW //
 qed-.
 
 lemma cnr_inv_abst: ∀a,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃ⓛ{a}V.T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃V⦄ ∧ ⦃G, L.ⓛV⦄ ⊢ 𝐍⦃T⦄.
 #a #G #L #V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct //
+[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2 by cpr_pair_sn/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2 by cpr_bind/ -HT2 #H destruct //
 ]
 qed-.
 
 lemma cnr_inv_abbr: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃-ⓓV.T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃V⦄ ∧ ⦃G, L.ⓓV⦄ ⊢ 𝐍⦃T⦄.
 #G #L #V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct //
+[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2 by cpr_pair_sn/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2 by cpr_bind/ -HT2 #H destruct //
 ]
 qed-.
 
 lemma cnr_inv_zeta: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃+ⓓV.T⦄ → ⊥.
 #G #L #V #T #H elim (is_lift_dec T 0 1)
 [ * #U #HTU
-  lapply (H U ?) -H /2 width=3/ #H destruct
+  lapply (H U ?) -H /2 width=3 by cpr_zeta/ #H destruct
   elim (lift_inv_pair_xy_y … HTU)
 | #HT
-  elim (cpr_delift G (⋆) V T (⋆. ⓓV) 0) // #T2 #T1 #HT2 #HT12
-  lapply (H (+ⓓV.T2) ?) -H /4 width=1/ -HT2 #H destruct /3 width=2/
+  elim (cpr_delift G (⋆) V T (⋆. ⓓV) 0) //
+  #T2 #T1 #HT2 #HT12 lapply (H (+ⓓV.T2) ?) -H /4 width=1 by tpr_cpr, cpr_bind/ -HT2
+  #H destruct /3 width=2 by ex_intro/
 ]
 qed-.
 
 lemma cnr_inv_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃ⓐV.T⦄ → ∧∧ ⦃G, L⦄ ⊢ 𝐍⦃V⦄ & ⦃G, L⦄ ⊢ 𝐍⦃T⦄ & 𝐒⦃T⦄.
 #G #L #V1 #T1 #HVT1 @and3_intro
-[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
+[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1 by cpr_pair_sn/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1 by cpr_flat/ -HT2 #H destruct //
 | 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}ⓝW1.V1.U1) ?) -H /3 width=1/ #H destruct
+    lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3 by tpr_cpr, cpr_theta/ -HV12 #H destruct
+  | lapply (H (ⓓ{a}ⓝW1.V1.U1) ?) -H /3 width=1 by tpr_cpr, cpr_beta/ #H destruct
 ]
 qed-.
 
 lemma cnr_inv_tau: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃ⓝV.T⦄ → ⊥.
-#G #L #V #T #H lapply (H T ?) -H /2 width=1/ #H
-@discr_tpair_xy_y //
+#G #L #V #T #H lapply (H T ?) -H
+/2 width=4 by cpr_tau, discr_tpair_xy_y/
 qed-.
 
 (* Basic properties *********************************************************)