Step
*
of Lemma
subtype-set
(T:Type × (T ⟶ Set{i:l})) ⊆r Set{i:l}
BY
{ (InstLemma `set-ext` [] THEN Auto) }
Latex:
Latex:
(T:Type \mtimes{} (T {}\mrightarrow{} Set\{i:l\})) \msubseteq{}r Set\{i:l\}
By
Latex:
(InstLemma `set-ext` [] THEN Auto)
Home
Index