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

At: remove is member 1 1 2 2 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) remove(eq;y;v) x(eq) v
9. eq(y,u) = false
10. eq(x,u) = true
11. true
12. eq(x,u) = false

x(eq) v
By: HypSubst -3 -1
Generated subgoal:

112. true = false
x(eq) v

About:
listboolbfalsebtrueassertapplyuniverseequalimplies

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