(* Properties with push for model evaluation ********************************)
-lemma tm_vpush_vlift_join_O (h) (v) (T): â\87¡[0]⫯{TM h}[0â\86\90T]v â\89\90 ⇡[0←↑[1]T]v.
+lemma tm_vpush_vlift_join_O (h) (v) (T): â\87¡[0]⫯{TM h}[0â\86\90T]v â\8a\9c ⇡[0←↑[1]T]v.
#h #v #T #i
elim (eq_or_gt i) #Hi destruct
[ >mf_vpush_eq >mf_vlift_rw >vpush_eq //