---

Step * 1 of Lemma assert_of_eq_pair


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|))
BY
{ ((RW bool_to_propC 0 
THENM New [`b1';`b2'] (D 4) 
THENM New [`a1';`a2'] (D 3)) THENA Auto) }

1
1. s : DSet
2. t : DSet
3. a1 : |s|
4. a2 : |t|
5. b1 : |s|
6. b2 : |t|
⊢ uiff(((fst(<a1, a2>)) = (fst(<b1, b2>)) ∈ |s|) ∧ ((snd(<a1, a2>)) = (snd(<b1, b2>)) ∈ |t|);<a1, a2> = <b1, b2> ∈ (|s| \000C× |t|))

---

Latex:

---

Latex:

1.  s  :  DSet
2.  t  :  DSet
3.  a  :  |s|  \mtimes{}  |t|
4.  b  :  |s|  \mtimes{}  |t|
\mvdash{}  uiff(\muparrow{}(((fst(a))  (=\msubb{})  (fst(b)))  \mwedge{}\msubb{}  ((snd(a))  (=\msubb{})  (snd(b))));a  =  b)


By

---

Latex:
((RW  bool\_to\_propC  0 
THENM  New  [`b1';`b2']  (D  4) 
THENM  New  [`a1';`a2']  (D  3))  THENA  Auto)

---

Home Index