-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.
-/4 width=6 by lifts_div4, at_div_id_dx, at_div_pn/ qed-.
+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.
+/4 width=6 by lifts_div4, pr_pat_div_id_dx, pr_pat_div_push_next/ qed-.