Nuprl - Pf ioa_univ

A:ioa{i:l}(). A ioa{i':l}

By: Assert (T:Type. Collection(T) Collection(T))

Generated subgoals:

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

2 1. T:Type{i}. Collection{i}(T) Collection{i'}(T)
A:ioa{i:l}(). A ioa{i':l}

About:

1	`T:Type{i}. Collection{i}(T) Collection{i'}(T)`
2	1. `T:Type{i}. Collection{i}(T) Collection{i'}(T)` `A:ioa{i:l}(). A ioa{i':l}`