#B2 #A2 #_ #_ @or_intror #H destruct
| #B1 #A1 #IHB1 #IHA1 #A2 elim A2 -A2
[ -IHB1 -IHA1 @or_intror #H destruct
| #B2 #A2 #_ #_ elim (IHB1 B2) -IHB1
[ #H destruct elim (IHA1 A2) -IHA1
#B2 #A2 #_ #_ @or_intror #H destruct
| #B1 #A1 #IHB1 #IHA1 #A2 elim A2 -A2
[ -IHB1 -IHA1 @or_intror #H destruct
| #B2 #A2 #_ #_ elim (IHB1 B2) -IHB1
[ #H destruct elim (IHA1 A2) -IHA1