---

Step * of Lemma cWO-rel_wf

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (cWO-rel(R) ∈ n:ℕ ⟶ (ℕn ⟶ (T?)) ⟶ (T?) ⟶ ℙ)
BY
{ (ProveWfLemma THEN All Reduce⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (cWO-rel(R)  \mmember{}  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  (T?))  {}\mrightarrow{}  (T?)  {}\mrightarrow{}  \mBbbP{})


By

---

Latex:
(ProveWfLemma  THEN  All  Reduce\mcdot{}  THEN  Auto)

---

Home Index