Step
*
of Lemma
valuetype__tree
∀[E:Type]. value-type(tree(E))
BY
{ (Auto THEN RWO "treeco-ext" 0 THEN Auto) }
Latex:
Latex:
\mforall{}[E:Type].  value-type(tree(E))
By
Latex:
(Auto  THEN  RWO  "treeco-ext"  0  THEN  Auto)
Home
Index