---

Step * of Lemma assert_of_eq_pair

∀[s,t:DSet]. ∀[a,b:|s| × |t|].  uiff(↑(a =b b);a = b ∈ (|s| × |t|))
BY
{ ((RepD THENM Unfold `eq_pair` 0) THENA Auto) }

1
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|))

---

Latex:

---

Latex:
\mforall{}[s,t:DSet].  \mforall{}[a,b:|s|  \mtimes{}  |t|].    uiff(\muparrow{}(a  =\msubb{}  b);a  =  b)


By

---

Latex:
((RepD  THENM  Unfold  `eq\_pair`  0)  THENA  Auto)

---

Home Index