#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
#L1 #L2 #W #V #W1 #V2 #l #HV #HW #_ #_ #_ #IHL12 -W1 -V2
elim (snv_fwd_aaa … HV) -HV #A #HV
#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
#L1 #L2 #W #V #W1 #V2 #l #HV #HW #_ #_ #_ #IHL12 -W1 -V2
elim (snv_fwd_aaa … HV) -HV #A #HV