Nuprl - Pf not not rw 1 1 1

(7steps) PrintForm Definitions core 3 jlc Sections Support(jlc) Doc

At: not not rw 1 1 1

1. T: Type
2. P: TProp
3. x: T
4. P(x)

P(x) P(x)

By: Auto

Generated subgoal:

1 5. P(x)
P(x)

About:

(7steps) PrintForm Definitions core 3 jlc Sections Support(jlc) Doc