Nuprl - Pf decidable list exists 1 2 1 1

1. T: Type
2. P: TProp
3. L: T List
4. x:T. Dec(P(x))
5. u: T
6. v: T List
7. Dec(xv.P(x))

P(u) xv.P(x) (P(u) xv.P(x))

By: Witness4 u

Generated subgoal:

1 4. u: T
5. v: T List
6. Dec(xv.P(x))
7. Dec(P(u))
P(u) xv.P(x) (P(u) xv.P(x))

About: