PrintForm Definitions mb collection Sections GenAutomata Doc

At: member col list prod

T:Type, l:Collection(T) List, x:T List. x col_list_prod(l) ||x|| = ||l|| & (i:. i < ||x|| x[i] l[i])
By:
RW ColMemberC 0
THEN
ExRepD
THEN
BackThruSomeHyp
Generated subgoals:

None

About:
listless_thanuniverseequalimpliesall

PrintForm Definitions mb collection Sections GenAutomata Doc