Step
*
of Lemma
stump_wf
∀[T:Type]. ∀[t:wfd-tree(T)].  (stump(t) ∈ n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹)
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[T:Type].  \mforall{}[t:wfd-tree(T)].    (stump(t)  \mmember{}  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbB{})
By
Latex:
ProveWfLemma
Home
Index