Nuprl - Pf lang_union

1. Alph: Type
2. L: Alph*Prop
3. M: Alph*Prop
4. N: Alph*Prop
5. l: Alph*

(l.L(l) (l.M(l) & N(l))(l))(l) (l.(l.L(l) M(l))(l) & (l.L(l) N(l))(l))(l)

By: Reduce 0 THEN GenUnivCD

Generated subgoals:

1 6. L(l) M(l) & N(l)
L(l) M(l)

2 6. L(l) M(l) & N(l)
L(l) N(l)

3 6. L(l) M(l) & L(l) N(l)
L(l) M(l) & N(l)

About: