-[ /5 width=5 by lfsx_lfdeq_trans, lfpxs_step_dx, lfdeq_pair/
-| @lfsx_lfpx_trans
- [2: @(IHV0 … HnV02 K0 … I) -IHV0 -HnV02
- [ /2 width=3 by lfpxs_cpx_trans/
- |
- |
- ]
- |1: skip
- |3: @lfpx_pair /2 width=3 by lfpx_cpx_conf/
+[ /5 width=5 by lfsx_lfdeq_trans, lpxs_trans, lfdeq_pair/
+| @(IHV0 … HnV02) -IHV0 -HnV02
+ [
+ | /3 width=3 by lfsx_lpxs_trans, lfsx_cpxs_trans/
+ | /2 width=3 by lpxs_trans/
+ ]
+
+(*
+ @(lfsx_lpxs_trans … (K0.ⓑ{I}V2))
+ [ @(IHV0 … HnV02 … HK10) -IHV0 -HnV02
+ [
+ | /2 width=3 by lfsx_cpxs_trans/
+ ]
+ |