Nuprl - Pf not not rw 1 1 1 1

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

At: not not rw 1 1 1 1

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

P(x)

By: Analyze 0

Generated subgoal:

1 6. P(x)
False

About:

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