-lemma lifts_div4_one: â\88\80f,Tf,T. â¬\86*[â\86\91f] Tf â\89¡ T →
- â\88\80T1. â¬\86*[1] T1 â\89¡ T →
- â\88\83â\88\83T0. â¬\86*[1] T0 â\89¡ Tf & â¬\86*[f] T0 â\89¡ T1.
+lemma lifts_div4_one: â\88\80f,Tf,T. â¬\86*[⫯f] Tf â\89\98 T →
+ â\88\80T1. â¬\86*[1] T1 â\89\98 T →
+ â\88\83â\88\83T0. â¬\86*[1] T0 â\89\98 Tf & â¬\86*[f] T0 â\89\98 T1.