Nuprl - Pf ioa_univ_lemma 1

(3steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

At: ioa univ lemma 1

T:Type{i}. Collection{i}(T) Collection{i'}(T)

By: Unfold `subtype` 0 THEN BackThru Thm* T:Type{i'}, c:Collection{i}(T). c Collection{i'}(T)

Generated subgoals:

None

About:

(3steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc