X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Fmodels%2Ftm.ma;h=613d67a7e4580f02b2669952bceb42a3edf5ea43;hp=00358c9a2da3d488bdec6734430fe3d2a8a6a2ab;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hpb=3b7b8afcb429a60d716d5226a5b6ab0d003228b1

diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/tm.ma b/matita/matita/contribs/lambdadelta/apps_2/models/tm.ma
index 00358c9a2..613d67a7e 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/models/tm.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/models/tm.ma
@@ -20,11 +20,11 @@ include "apps_2/models/model.ma".
 
 definition tm_dd ≝ term.
 
-definition tm_sq (h) (T1) (T2) ≝  ⦃⋆,⋆⦄ ⊢ T1 ⬌*[h] T2.
+definition tm_sq (h) (T1) (T2) ≝  ❪⋆,⋆❫ ⊢ T1 ⬌*[h] T2.
 
 definition tm_sv (s) ≝ ⋆s.
 
-definition tm_co (p) (V) (T) ≝ ⓓ{p}V.(↑[1]T).
+definition tm_co (p) (V) (T) ≝ ⓓ[p]V.(↑[1]T).
 
 definition tm_ap (V) (T) ≝ ⓐV.T.
 
@@ -42,7 +42,7 @@ defined-.
 
 (* Basic properties *********************************************************)
 
-lemma tm_co_rw (h) (p) (V) (T): V⊕{TM h}[p]T = ⓓ{p}V.(↑[1]T).
+lemma tm_co_rw (h) (p) (V) (T): V⊕{TM h}[p]T = ⓓ[p]V.(↑[1]T).
 // qed.
 
 lemma tm_ti_sort (h) (gv) (lv): ∀s. ⟦⋆s⟧{TM h}[gv,lv] = sv … s.
@@ -55,5 +55,5 @@ lemma tm_ti_gref (h): ∀gv,lv,l. ⟦§l⟧{TM h}[gv,lv] = gv l.
 // qed.
 
 lemma tm_ti_bind (h) (p) (I): ∀gv,lv,V,T.
-                              ⟦ⓑ{p,I}V.T⟧{TM h}[gv,lv] = ⓑ{p,I}⟦V⟧[gv,lv].⟦T⟧{TM h}[⇡[0]gv,⇡[0←#0]lv].
+                              ⟦ⓑ[p,I]V.T⟧{TM h}[gv,lv] = ⓑ[p,I]⟦V⟧[gv,lv].⟦T⟧{TM h}[⇡[0]gv,⇡[0←#0]lv].
 // qed.