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