- [4: /3 width=2 by seq_sym, md/ | skip
- |3: @IHT /2 width=1 by li_abbr/ | skip ] -T1
- /4 width=1 by ti_comp, vlift_comp, (* 2x *) veq_refl/
+ [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
+ /4 width=1 by ti_comp, vpush_comp, (* 2x *) veq_refl/