X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Fmodels%2Ftm_props.ma;h=1f3c49413751079a74cb8f929037afa1e43f7c5e;hp=280bd8e51086a20e3738cf54996ee13e9a0a31aa;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hpb=3b7b8afcb429a60d716d5226a5b6ab0d003228b1

diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma b/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma
index 280bd8e51..1f3c49413 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma
@@ -30,7 +30,7 @@ lemma pippo (h) (gv) (lv) (T): ●[gv,lv]T = ⟦T⟧{TM h}[gv,lv].
 lemma tm_mi (h) (gv1) (gv2) (lv1) (lv2) (p) (W) (T):
             ⟦W⟧[gv1,lv1] ≗{TM h} ⟦W⟧[gv2,lv2] →
             (∀d. ⟦T⟧[gv1,⫯[0←d]lv1] ≗ ⟦T⟧[gv2,⫯[0←d]lv2]) →
-            ⟦ⓛ{p}W.T⟧[gv1,lv1] ≗ ⟦ⓛ{p}W.T⟧[gv2,lv2].
+            ⟦ⓛ[p]W.T⟧[gv1,lv1] ≗ ⟦ⓛ[p]W.T⟧[gv2,lv2].
 #h #gv1 #gv2 #lv1 #lv2 #p #W #T #HW #HT
 >tm_ti_bind >tm_ti_bind
 @(cpcs_bind1 … HW)
@@ -46,7 +46,7 @@ lapply (HT (#0)) -HT #HT
 *)
 
 lemma tm_md (h) (p) (gv) (lv) (V) (T):
-            ⓓ{p}V.⟦T⟧{TM h}[⇡[0]gv,⇡[0←#0]lv] ≗{TM h} V⊕{TM h}[p]⟦T⟧{TM h}[gv,⫯{TM h}[0←V]lv].
+            ⓓ[p]V.⟦T⟧{TM h}[⇡[0]gv,⇡[0←#0]lv] ≗{TM h} V⊕{TM h}[p]⟦T⟧{TM h}[gv,⫯{TM h}[0←V]lv].
 #h #p #gv #lv #V #T
 >tm_co_rw >(mf_lifts_basic_SO_dx T 0)
 >(mf_comp … T) in ⊢ (???%);
@@ -62,7 +62,7 @@ lemma tm_me (h) (gv) (lv) (U) (T):
 /4 width=1 by cpc_cpcs, cpm_eps, or_introl/ qed.
 
 lemma tm_mb (h) (p) (gv) (lv) (d) (W) (T):
-            d@⟦ⓛ{p}W.T⟧[gv,lv] ≗{TM h} d⊕[p]⟦T⟧[gv,⫯[0←d]lv].
+            d@⟦ⓛ[p]W.T⟧[gv,lv] ≗{TM h} d⊕[p]⟦T⟧[gv,⫯[0←d]lv].
 #h #p #gv #lv #d #W #T
 @cpcs_repl [5: @tm_md |4: /4 width=2 by cpc_cpcs, cpm_beta, or_intror/ |1,2: skip ]
 /5 width=1 by cpcs_bind1, cpc_cpcs, cpm_eps, or_introl/