- nDestructTac: Sys.break handled in two places

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / reducibility / cnf_lift.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma
index e0d8d57bb4021d6f1e907934de5e3c43c8498c4a..3aefb3643de2e5f8971c7c9bb18f003b1f569862 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma
@@ -20,7 +20,7 @@ include "basic_2/reducibility/cnf.ma".
 (* Advanced inversion lemmas ************************************************)
 
 (* Basic_1: was only: nf2_csort_lref *)
-lemma cnf_lref_atom: ∀L,i. ⇩[0, i] L ≡ ⋆ → L  ⊢ 𝐍[#i].
+lemma cnf_lref_atom: ∀L,i. ⇩[0, i] L ≡ ⋆ → L  ⊢ 𝐍⦃#i⦄.
 #L #i #HLK #X #H
 elim (cpr_inv_lref1 … H) // *
 #K0 #V0 #V1 #HLK0 #_ #_ #_
@@ -28,7 +28,7 @@ lapply (ldrop_mono … HLK … HLK0) -L #H destruct
 qed.
 
 (* Basic_1: was: nf2_lref_abst *)
-lemma cnf_lref_abst: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓛV → L ⊢ 𝐍[#i].
+lemma cnf_lref_abst: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓛV → L ⊢ 𝐍⦃#i⦄.
 #L #K #V #i #HLK #X #H
 elim (cpr_inv_lref1 … H) // *
 #K0 #V0 #V1 #HLK0 #_ #_ #_
@@ -36,14 +36,14 @@ lapply (ldrop_mono … HLK … HLK0) -L #H destruct
 qed.
 
 (* Basic_1: was: nf2_abst *)
-lemma cnf_abst: ∀I,L,V,W,T. L ⊢ 𝐍[W] → L. ⓑ{I} V ⊢ 𝐍[T] → L ⊢ 𝐍[ⓛW.T].
+lemma cnf_abst: ∀I,L,V,W,T. L ⊢ 𝐍⦃W⦄ → L. ⓑ{I} V ⊢ 𝐍⦃T⦄ → L ⊢ 𝐍⦃ⓛW.T⦄.
 #I #L #V #W #T #HW #HT #X #H
 elim (cpr_inv_abst1 … H I V) -H #W0 #T0 #HW0 #HT0 #H destruct
 >(HW … HW0) -W0 >(HT … HT0) -T0 //
 qed.
 
 (* Basic_1: was only: nf2_appl_lref *)
-lemma cnf_appl_simple: ∀L,V,T. L ⊢ 𝐍[V] → L ⊢ 𝐍[T] → 𝐒[T] → L ⊢ 𝐍[ⓐV.T].
+lemma cnf_appl_simple: ∀L,V,T. L ⊢ 𝐍⦃V⦄ → L ⊢ 𝐍⦃T⦄ → 𝐒⦃T⦄ → L ⊢ 𝐍⦃ⓐV.T⦄.
 #L #V #T #HV #HT #HS #X #H
 elim (cpr_inv_appl1_simple … H ?) -H // #V0 #T0 #HV0 #HT0 #H destruct
 >(HV … HV0) -V0 >(HT … HT0) -T0 //
@@ -53,7 +53,7 @@ qed.
 
 (* Basic_1: was: nf2_lift *)
 lemma cnf_lift: ∀L0,L,T,T0,d,e.
-                L ⊢ 𝐍[T] → ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → L0 ⊢ 𝐍[T0].
+                L ⊢ 𝐍⦃T⦄ → ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → L0 ⊢ 𝐍⦃T0⦄.
 #L0 #L #T #T0 #d #e #HLT #HL0 #HT0 #X #H
 elim (cpr_inv_lift … HL0 … HT0 … H) -L0 #T1 #HT10 #HT1
 <(HLT … HT1) in HT0; -L #HT0