Nuprl - Pf decidable disjoint 1 2 1

1. T: Type
2. eq: TT
3. L1: T List
4. L2: T List
5. u: T
6. v: T List
7. Dec(xv.x(eq) L2)

Dec(u(eq) L2 & xv.x(eq) L2)

By: Decide u(eq) L2

Generated subgoals:

1 8. u(eq) L2
Dec(u(eq) L2 & xv.x(eq) L2)

2 8. u(eq) L2
Dec(u(eq) L2 & xv.x(eq) L2)

About:

1	8. `u(eq) L2` `Dec(u(eq) L2 & xv.x(eq) L2)`
2	8. `u(eq) L2` `Dec(u(eq) L2 & xv.x(eq) L2)`