| #a; #a'; #b; #b'; #H1; #H2; napply mk_iff; #H; #w
[ napply (if … H2); napply H; napply (fi … H1); nassumption
| napply (fi … H2); napply H; napply (if … H1); nassumption]##]
| #a; #a'; #b; #b'; #H1; #H2; napply mk_iff; #H; #w
[ napply (if … H2); napply H; napply (fi … H1); nassumption
| napply (fi … H2); napply H; napply (if … H1); nassumption]##]