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

At: is member sublist lemma 1 1 1
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) = true
10. true
11. u(eq) M
12. v(eq)M

x(eq) M
By: FwdThru Thm* P:. P P = true [9]
Generated subgoal:

113. eq(x,u)
x(eq) M

About:
listboolbtrueassertapplyuniverseequalimplies

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