X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Fmodels%2Ftm_props.ma;h=640de8c4f63d505a447b3d91771e2a2d872b6ccc;hb=77479649510792efe4d9cbff508e118360862594;hp=1777a2d000a874f4f603ac57a1484b0082a726ae;hpb=12dc655b7f5321b33b93a310d53e23e60e090caa;p=helm.git

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 1777a2d00..640de8c4f 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma
@@ -24,7 +24,7 @@ include "apps_2/models/tm_vpush.ma".
 lemma cpcs_repl (h) (G) (L): replace_2 … (cpcs h G L) (cpcs h G L) (cpcs h G L).
 /3 width=5 by cpcs_trans, cpcs_sym/ qed-.
 (*
-lemma pippo (h) (gv) (lv) (T): ●[gv,lv]T = ⟦T⟧{TM h}[gv,lv].
+lemma pippo (h) (gv) (lv) (T): ■[gv,lv]T = ⟦T⟧{TM h}[gv,lv].
 // qed.
 
 lemma tm_mi (h) (gv1) (gv2) (lv1) (lv2) (p) (W) (T):
@@ -38,7 +38,7 @@ lemma tm_mi (h) (gv1) (gv2) (lv1) (lv2) (p) (W) (T):
 
 
 <pippo in ⊢ (????%?); >(mf_comp … T) in ⊢ (????%?);
-[2: ;;tm_vpush_vlift_join_O
+[2: @tm_vpush_vlift_join_O
 
 <pippo in ⊢ (????%?);