Equality of pairs

Stream: new members

[Torger Olson]

If I have an equality or pairs (of sets) : (a, b) = (c, d) how do I get a = c?

[Ruben Van de Velde]

Some lemma called ext_iff, probably

[Johan Commelin]

congr_arg prod.fst h, where h is your proof of (a,b) = (c,d).

[Marcus Rossel]

IIRC the injection tactic might also work for this.