---

Step * 1 of Lemma mem-mk-set_wf


1. T : Type
2. f : T ⟶ coSet{i:l}
3. t : T
⊢ seteqweaken(f t) Ax ∈ seteq(f t;f t)
BY
{ (InstLemma `seteqweaken_wf` [f t;⌜f t⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  coSet\{i:l\}
3.  t  :  T
\mvdash{}  seteqweaken(f  t)  Ax  \mmember{}  seteq(f  t;f  t)


By

---

Latex:
(InstLemma  `seteqweaken\_wf`  [f  t;\mkleeneopen{}f  t\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index