---

Step * of Lemma wfFormAux-unique

∀[C:Type]. ∀[f:Form(C)]. ∀[b:𝔹].  ((↑(wfFormAux(f) b)) ⇒ termForm(f) = b)
BY
{ (Auto THEN RepeatFor 3 (MoveToConcl (-1))) }

1
1. C : Type
⊢ ∀f:Form(C). ∀b:𝔹.  ((↑(wfFormAux(f) b)) ⇒ termForm(f) = b)

---

Latex:

---

Latex:
\mforall{}[C:Type].  \mforall{}[f:Form(C)].  \mforall{}[b:\mBbbB{}].    ((\muparrow{}(wfFormAux(f)  b))  {}\mRightarrow{}  termForm(f)  =  b)


By

---

Latex:
(Auto  THEN  RepeatFor  3  (MoveToConcl  (-1)))

---

Home Index