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

At: append commutes under is member 2 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. M: T List
9. x: T
10. x(eq) (M @ L)
11. x(eq) M x(eq) L

x(eq) (L @ M)

By: BackThru Thm* eq:{T}, L,M:T List, x:T. x(eq) (L @ M) x(eq) L x(eq) M

Generated subgoal:

1 x(eq) L x(eq) M

About:
listboolassertapplyfunctionuniversememberimpliesorall

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