(7steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc

At: is member sublist lemma 1 1 2
1. T: Type
2. eq: {T=}
3. x: T
4. L: T List
5. M: T List
6. u: T
7. v: T List
8. x(eq) v v(eq)M x(eq) M
9. eq(x,u) = false
10. x(eq) v
11. u(eq) M
12. v(eq)M

x(eq) M
By: HypBackchain
Generated subgoals:

None

About:
listboolbfalseassertapplyuniverseequalimplies

(7steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc