update in ground_2, static_2, basic_2, apps_2, alpha_1

[helm.git] / matita / matita / contribs / lambdadelta / apps_2 / models / tm.ma

diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/tm.ma b/matita/matita/contribs/lambdadelta/apps_2/models/tm.ma
index 00358c9a2da3d488bdec6734430fe3d2a8a6a2ab..613d67a7e4580f02b2669952bceb42a3edf5ea43 100644 (file)
--- 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) â\89\9d  â¦\83â\8b\86,â\8b\86â¦\84 ⊢ T1 ⬌*[h] T2.
+definition tm_sq (h) (T1) (T2) â\89\9d  â\9dªâ\8b\86,â\8b\86â\9d« ⊢ 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.