---

Step * 2 1 of Lemma setmem-productset


1. T : Type
2. a1 : T ⟶ coSet{i:l}
3. T1 : Type
4. b1 : T1 ⟶ coSet{i:l}
5. p : coSet{i:l}
6. u : coSet{i:l}
7. v : coSet{i:l}
8. t1 : T
9. seteq(u;a1 t1)
10. t : T1
11. seteq(v;b1 t)
12. seteq(p;(u,v))
⊢ seteq(p;(a1 t1,b1 t))
BY
{ (RWO "-1" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  a1  :  T  {}\mrightarrow{}  coSet\{i:l\}
3.  T1  :  Type
4.  b1  :  T1  {}\mrightarrow{}  coSet\{i:l\}
5.  p  :  coSet\{i:l\}
6.  u  :  coSet\{i:l\}
7.  v  :  coSet\{i:l\}
8.  t1  :  T
9.  seteq(u;a1  t1)
10.  t  :  T1
11.  seteq(v;b1  t)
12.  seteq(p;(u,v))
\mvdash{}  seteq(p;(a1  t1,b1  t))


By

---

Latex:
(RWO  "-1"  0  THEN  Auto)

---

Home Index