Nuprl - Pf is member sublist lemma 1

1. T: Type
2. eq: {T=}
3. x: T
4. L: T List
5. M: T List
6. x(eq) L
7. L(eq)M

x(eq) M

By: ListInd 4 THEN Reduce 0

Generated subgoal:

1 6. u: T
7. v: T List
8. x(eq) v v(eq)M x(eq) M
9. if eq(x,u) true else x(eq) v fi
10. u(eq) M
11. v(eq)M
x(eq) M

About: