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

At: is member append lemma1 1 2 2 1 1 1 1 1

1. T: Type
2. eq: {T}
3. eq TT
4. x:T. eq(x,x)
5. x,y:T. eq(x,y) eq(y,x)
6. x,y,z:T. eq(x,y) eq(y,z) eq(x,z)
7. L: T List
8. x: T
9. u: T
10. v: T List
11. eq(x,u) = false
12. x(eq) v
13. M: T List
14. N: T List
15. y: T
16. eq(x,y)
17. v = (M @ (y.N))

u.v = ((u.M) @ (y.N))

By:
HypSubst -1 0
THEN
Reduce 0


Generated subgoal:

1 u.(M @ (y.N)) = u.(M @ (y.N))

About:
listconsboolbfalseassertapplyfunctionuniverseequalmemberimpliesall

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