is mentioned by

Thm* x,z,y,w:T List. ||x|| = ||z|| ||y|| = ||w|| (x @ y) = (z @ w) x = z & y = w	[append_one_one]
Thm* a,b:T List, x:T. [x] = (a @ b) a = nil & b = [x] b = nil & a = [x]	[append_is_singleton]
Thm* a,c,b,d:T List. (a @ b) = (c @ d) (e:T List. a = (c @ e) & d = (e @ b) c = (a @ e) & b = (e @ d))	[equal_appends]
Thm* A,B:T List, x,y:T. x before y A @ B x before y A x before y B (x A) & (y B)	[l_before_append_iff]

In prior sections: core bool 1 int 2 list 1 sqequal 1 prog 1 rel 1 mb nat mb list 1 num thy 1 mb list 2

Try larger context: Graphs