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

At: not is member remove lemma 1 1 1 1 1 1 1
1. T: Type
2. eq: {T=}
3. x: T
4. y: T
5. L: T List
6. u: T
7. v: T List
8. x(eq) v x(eq) remove(eq;y;v)
9. eq(x,u) = true
10. true
11. eq(y,u) = true
12. eq(y,u)
13. eq(x,u)
14. x = u
15. y = u

eq(x,y)
By: BackThru Thm* T:Type, eq:{T=}. (x,y:T. eq(x,y) x = y) & eq TT
Generated subgoal:

1 x = y

About:
listboolbtrueassertapplyuniverseequalimplies

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