---

Step * of Lemma FormSet_wf

∀[C:Type]. ∀[var:Atom]. ∀[phi:Form(C)].  ({var | phi} ∈ Form(C))
BY
{ DepprodCoDatatypeConstructorWf `Form_size` }

---

Latex:

---

Latex:
\mforall{}[C:Type].  \mforall{}[var:Atom].  \mforall{}[phi:Form(C)].    (\{var  |  phi\}  \mmember{}  Form(C))


By

---

Latex:
DepprodCoDatatypeConstructorWf  `Form\_size`

---

Home Index