---

Step * of Lemma coSet-seteq-Set

∀[s:Set{i:l}]. ∀[z:coSet{i:l}].  z ∈ Set{i:l} supposing seteq(z;s)
BY
{ ((D 0 THENA Auto) THEN Unfold `Set` 1 THEN WElim 1) }

1
1. a : Type
2. f : a ⟶ W(Type;a.a)
3. ∀b:a. ∀[z:coSet{i:l}]. z ∈ Set{i:l} supposing seteq(z;f b)
⊢ Ax ∈ ∀[z@0:coSet{i:l}]. z@0 ∈ Set{i:l} supposing seteq(z@0;Wsup(a;f))

---

Latex:

---

Latex:
\mforall{}[s:Set\{i:l\}].  \mforall{}[z:coSet\{i:l\}].    z  \mmember{}  Set\{i:l\}  supposing  seteq(z;s)


By

---

Latex:
((D  0  THENA  Auto)  THEN  Unfold  `Set`  1  THEN  WElim  1)

---

Home Index