Nuprl - Pf list all append lemma 2 1 2

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

P(u) & xv.P(x) (M:T List. xM.P(x) P(u) & x(v @ M).P(x))

By: Auto

Generated subgoal:

1 7. P(u)
8. xv.P(x)
9. M: T List
10. xM.P(x)
x(v @ M).P(x)

About: