∀[s,t:DSet]. ∀[a,b:|s| × |t|]. uiff(↑(a =b b);a = b ∈ (|s| × |t|))
{ ((RepD THENM Unfold `eq_pair` 0) THENA Auto) }
1. s : DSet
2. t : DSet
3. a : |s| × |t|
4. b : |s| × |t|
⊢ uiff(↑(((fst(a)) (=b) (fst(b))) ∧b ((snd(a)) (=b) (snd(b))));a = b ∈ (|s| × |t|))