Step
*
of Lemma
unit_subtype_list
∀[T:Type]. (Unit ⊆r (T List))
BY
{ (Auto THEN InstLemma `list-ext` [⌜T⌝]⋅ THEN Auto) }
Latex:
Latex:
\mforall{}[T:Type].  (Unit  \msubseteq{}r  (T  List))
By
Latex:
(Auto  THEN  InstLemma  `list-ext`  [\mkleeneopen{}T\mkleeneclose{}]\mcdot{}  THEN  Auto)
Home
Index