(* Properties with relocation ***********************************************)
-lemma mf_lifts_basic_SO_dx (T) (j): â\88\80gv,lv. â\86\91[j,1]â\97\8f[gv,lv]T = â\97\8f[⇡[j]gv,⇡[j]lv]T.
+lemma mf_lifts_basic_SO_dx (T) (j): â\88\80gv,lv. â\86\91[j,1]â\96 [gv,lv]T = â\96 [⇡[j]gv,⇡[j]lv]T.
#T elim T -T * //
[ #p #I #V #T #IHV #IHT #j #gv #lv
>mf_bind >mf_bind >flifts_basic_bind