Nuprl - Pf auto2_lemma

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

(x:T. P(x)) (x:T. P(x))

By: Analyze 4

Generated subgoals:

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

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

About:

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