@(mq … H1M) [4,5: /3 width=2 by seq_sym, me/ |1,2: skip ] -L -V1
/2 width=1 by mr/
| #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV #IHW #IHT #HV2 #gv #lv #Hlv
@(mq … H1M) [4,5: /3 width=2 by seq_sym, ma, md/ |1,2: skip ]
@(seq_trans … H1M) [3: /3 width=1 by seq_sym, ma/ | skip ]
@(mq … H1M) [4,5: /3 width=2 by seq_sym, me/ |1,2: skip ] -L -V1
/2 width=1 by mr/
| #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV #IHW #IHT #HV2 #gv #lv #Hlv
@(mq … H1M) [4,5: /3 width=2 by seq_sym, ma, md/ |1,2: skip ]
@(seq_trans … H1M) [3: /3 width=1 by seq_sym, ma/ | skip ]