Step
*
of Lemma
real-vec-free_wf
∀[k:ℕ]. ∀[L:ℝ^k List].  (real-vec-free(k;L) ∈ ℙ)
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[L:\mBbbR{}\^{}k  List].    (real-vec-free(k;L)  \mmember{}  \mBbbP{})
By
Latex:
ProveWfLemma
Home
Index