X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Ftrf.ma;h=6d6993de3f137b561d551be5533c83d182ead802;hb=a2144f09d1bd7022c1f2dfd4909a1fb9772c8d56;hp=83306d2de3656fbe3b36b89160a5b9960cabc71a;hpb=a8c166f1e1baeeae04553058bd179420ada8bbe7;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma
index 83306d2de..6d6993de3 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma
@@ -23,7 +23,7 @@ inductive trf: predicate term ≝
 | trf_appl_sn: ∀V,T.   trf V → trf (ⓐV. T)
 | trf_appl_dx: ∀V,T.   trf T → trf (ⓐV. T)
 | trf_abbr   : ∀V,T.           trf (ⓓV. T)
-| trf_cast   : ∀V,T.           trf (ⓣV. T)
+| trf_cast   : ∀V,T.           trf (ⓝV. T)
 | trf_beta   : ∀V,W,T. trf (ⓐV. ⓛW. T)
 .
 
@@ -33,7 +33,7 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-fact trf_inv_atom_aux: ∀I,T. 𝐑[T] → T =  ⓪{I} → False.
+fact trf_inv_atom_aux: ∀I,T. 𝐑⦃T⦄ → T =  ⓪{I} → ⊥.
 #I #T * -T
 [ #V #T #_ #H destruct
 | #V #T #_ #H destruct
@@ -45,10 +45,10 @@ fact trf_inv_atom_aux: ∀I,T. 𝐑[T] → T =  ⓪{I} → False.
 ]
 qed.
 
-lemma trf_inv_atom: ∀I. 𝐑[⓪{I}] → False.
+lemma trf_inv_atom: ∀I. 𝐑⦃⓪{I}⦄ → ⊥.
 /2 width=4/ qed-.
 
-fact trf_inv_abst_aux: ∀W,U,T. 𝐑[T] → T =  ⓛW. U → 𝐑[W] ∨ 𝐑[U].
+fact trf_inv_abst_aux: ∀W,U,T. 𝐑⦃T⦄ → T =  ⓛW. U → 𝐑⦃W⦄ ∨ 𝐑⦃U⦄.
 #W #U #T * -T
 [ #V #T #HV #H destruct /2 width=1/
 | #V #T #HT #H destruct /2 width=1/
@@ -60,11 +60,11 @@ fact trf_inv_abst_aux: ∀W,U,T. 𝐑[T] → T =  ⓛW. U → 𝐑[W] ∨ 𝐑[U
 ]
 qed.
 
-lemma trf_inv_abst: ∀V,T. 𝐑[ⓛV.T] → 𝐑[V] ∨ 𝐑[T].
+lemma trf_inv_abst: ∀V,T. 𝐑⦃ⓛV.T⦄ → 𝐑⦃V⦄ ∨ 𝐑⦃T⦄.
 /2 width=3/ qed-.
 
-fact trf_inv_appl_aux: ∀W,U,T. 𝐑[T] → T =  ⓐW. U →
-                       ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → False).
+fact trf_inv_appl_aux: ∀W,U,T. 𝐑⦃T⦄ → T =  ⓐW. U →
+                       ∨∨ 𝐑⦃W⦄ | 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥).
 #W #U #T * -T
 [ #V #T #_ #H destruct
 | #V #T #_ #H destruct
@@ -77,5 +77,5 @@ fact trf_inv_appl_aux: ∀W,U,T. 𝐑[T] → T =  ⓐW. U →
 ]
 qed.
 
-lemma trf_inv_appl: ∀W,U. 𝐑[ⓐW.U] → ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → False).
+lemma trf_inv_appl: ∀W,U. 𝐑⦃ⓐW.U⦄ → ∨∨ 𝐑⦃W⦄ | 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥).
 /2 width=3/ qed-.