X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Ftnf.ma;h=294546af97d8bd8da1822ea74cffb6b4bdcb5480;hb=5ac2dc4e01aca542ddd13c02b304c646d8df9799;hp=6f6d99096942fbef746c84665aea4204504cee06;hpb=78d4844bcccb3deb58a3179151c3045298782b18;p=helm.git

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 6f6d99096..294546af9 100644
--- 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-.