Nuprl - Pf not_dec_is

1. A: Type
2. P: AProp
3. x:A. P(x) P(x)
4. (x:A. P(x)) (x:A. P(x))

(x:A. P(x)) (x:A. P(x))

By: Analyze 4

Generated subgoals:

1 4. x:A. P(x)
(x:A. P(x)) (x:A. P(x))

2 4. (x:A. P(x))
(x:A. P(x)) (x:A. P(x))

About:

1	4. `x:A. P(x)` `(x:A. P(x)) (x:A. P(x))`
2	4. `(x:A. P(x))` `(x:A. P(x)) (x:A. P(x))`