---

Step * of Lemma termForm_wf

∀[c:Type]. ∀[f:Form(c)].  (termForm(f) ∈ 𝔹)
BY
{ (Intros THEN Unfold `termForm` 0 THEN (InstLemma `Form_ind_wf_simple` [⌜c⌝]⋅ THENA Auto) THEN BHyp -1  THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[c:Type].  \mforall{}[f:Form(c)].    (termForm(f)  \mmember{}  \mBbbB{})


By

---

Latex:
(Intros
  THEN  Unfold  `termForm`  0
  THEN  (InstLemma  `Form\_ind\_wf\_simple`  [\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  BHyp  -1 
  THEN  Auto)

---

Home Index