- @(mr … H1M) [4,5: @(seq_sym … H1M) [ @(ma … H1M) | @(md … H1M) ] |1,2: skip ]
- @(mr … H1M) [4,5: @(seq_sym … H1M) [ @(mc … H1M) | @(ma … H1M) ] |1,2: skip ]
- [2: @IHV // |4: @(md … H1M) |1,3: skip ] -p -V1
- @(mc … H1M) [ /2 width=1 by lifts_SO_fwd_vlift/ ] -V -V2
- @(seq_trans … H1M) [2: @IHT /3 width=1 by li_abbr, veq_refl/ | skip ] -T1
- /4 width=1 by ti_comp_l, veq_refl, vlift_comp/
+ @(mq … H1M) [4,5: /3 width=2 by seq_sym, ma, md/ |1,2: skip ]
+ @(mq … H1M)
+ [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/