Nuprl - Pf col_all_iff

PrintForm Definitions mb collection Sections GenAutomata Doc

At: col all iff

T:Type, c:Collection(T), P:(TProp). (xc.P(x)) (x:T. x c P(x))

By: Unfold `col_all` 0 THEN BackThruSomeHyp THEN Trivial

Generated subgoals:

None

About:

PrintForm Definitions mb collection Sections GenAutomata Doc