- [4: /3 width=2 by seq_sym, md/ | skip
- |3: @IHT /2 width=1 by li_abbr/ | skip ] -T1
+ [4: /4 width=2 by seq_sym, md, mp/ |1: skip
+ |5: /4 width=2 by seq_sym, ma, mc/ |2: skip
+ ]
+ @(seq_trans … H1M) [2: @mh // | skip ]
+ @mc [3:|*: /2 width=1 by mr/ ]
+ @mp [3:|*: /2 width=1 by lifts_SO_fwd_vpush/ ]
+ @(seq_trans … H1M) [2: @IHT /2 width=1 by li_abbr/ | skip ] -T1