- nDestructTac: Sys.break handled in two places

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

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma
index 6f6d99096942fbef746c84665aea4204504cee06..294546af97d8bd8da1822ea74cffb6b4bdcb5480 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma
@@ -24,14 +24,14 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma tnf_inv_abst: ∀V,T. 𝐍[ⓛV.T] → 𝐍[V] ∧ 𝐍[T].
+lemma tnf_inv_abst: ∀V,T. 𝐍⦃ⓛV.T⦄ → 𝐍⦃V⦄ ∧ 𝐍⦃T⦄.
 #V1 #T1 #HVT1 @conj
 [ #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 //
 ]
 qed-.
 
-lemma tnf_inv_appl: ∀V,T. 𝐍[ⓐV.T] → ∧∧ 𝐍[V] & 𝐍[T] & 𝐒[T].
+lemma tnf_inv_appl: ∀V,T. 𝐍⦃ⓐV.T⦄ → ∧∧ 𝐍⦃V⦄ & 𝐍⦃T⦄ & 𝐒⦃T⦄.
 #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 //
@@ -42,7 +42,7 @@ lemma tnf_inv_appl: ∀V,T. 𝐍[ⓐV.T] → ∧∧ 𝐍[V] & 𝐍[T] & 𝐒[T].
 ]
 qed-.
 
-lemma tnf_inv_abbr: ∀V,T. 𝐍[ⓓV.T] → ⊥.
+lemma tnf_inv_abbr: ∀V,T. 𝐍⦃ⓓV.T⦄ → ⊥.
 #V #T #H elim (is_lift_dec T 0 1)
 [ * #U #HTU
   lapply (H U ?) -H /2 width=3/ #H destruct
@@ -53,7 +53,7 @@ lemma tnf_inv_abbr: ∀V,T. 𝐍[ⓓV.T] → ⊥.
 ]
 qed.
 
-lemma tnf_inv_cast: ∀V,T. 𝐍[ⓣV.T] → ⊥.
+lemma tnf_inv_cast: ∀V,T. 𝐍⦃ⓣV.T⦄ → ⊥.
 #V #T #H lapply (H T ?) -H /2 width=1/ #H
 @discr_tpair_xy_y //
 qed-.