Nuprl - Pf not not rw 1 1

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

At: not not rw 1 1

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

P(x) P(x)

By: Analyze -1

Generated subgoals:

1 4. P(x)
P(x) P(x)

2 4. P(x)
P(x) P(x)

About:

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