Step
*
of Lemma
test-prog-obj_wf
∀x:test-prog(). (test-prog-obj(x) ∈ test-Obj())
BY
{ MrecConstructorWf }
Latex:
Latex:
\mforall{}x:test-prog().  (test-prog-obj(x)  \mmember{}  test-Obj())
By
Latex:
MrecConstructorWf
Home
Index