Step * of Lemma valuetype__tree

[E:Type]. value-type(tree(E))
BY
(Auto THEN RWO "treeco-ext" THEN Auto) }


Latex:


Latex:
\mforall{}[E:Type].  value-type(tree(E))


By


Latex:
(Auto  THEN  RWO  "treeco-ext"  0  THEN  Auto)




Home Index