---

Step * 1 of Lemma wfFormAux-unique


1. C : Type
⊢ ∀f:Form(C). ∀b:𝔹.  ((↑(wfFormAux(f) b)) ⇒ termForm(f) = b)
BY
{ ((BLemma `Form-induction` THENW Auto)
   THEN RepUR ``wfFormAux termForm`` 0
   THEN Try (Folds ``termForm wfFormAux`` 0)
   THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  Type
\mvdash{}  \mforall{}f:Form(C).  \mforall{}b:\mBbbB{}.    ((\muparrow{}(wfFormAux(f)  b))  {}\mRightarrow{}  termForm(f)  =  b)


By

---

Latex:
((BLemma  `Form-induction`  THENW  Auto)
  THEN  RepUR  ``wfFormAux  termForm``  0
  THEN  Try  (Folds  ``termForm  wfFormAux``  0)
  THEN  Auto)

---

Home Index