Step
*
of Lemma
tree_subtype
∀[A,B:Type]. tree(A) ⊆r tree(B) supposing A ⊆r B
BY
{ ((UnivCD THENA Auto) THEN (D 0 THENA Auto) THEN SimpleDatatypeInduction (-1) THEN Auto) }
Latex:
Latex:
\mforall{}[A,B:Type]. tree(A) \msubseteq{}r tree(B) supposing A \msubseteq{}r B
By
Latex:
((UnivCD THENA Auto) THEN (D 0 THENA Auto) THEN SimpleDatatypeInduction (-1) THEN Auto)
Home
Index