---

Step * 1 1 of Lemma set_prod_wf


1. s : DSet
2. t : DSet
⊢ ∀[x,y:|s| × |t|].  uiff(↑(x =b y);x = y ∈ (|s| × |t|))
BY
{ ((RepD THENM  
 Simple (BLemma `assert_of_eq_pair`)) THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet
2.  t  :  DSet
\mvdash{}  \mforall{}[x,y:|s|  \mtimes{}  |t|].    uiff(\muparrow{}(x  =\msubb{}  y);x  =  y)


By

---

Latex:
((RepD  THENM   
  Simple  (BLemma  `assert\_of\_eq\_pair`))  THEN  Auto)

---

Home Index