C,A,B:T List. C 
A @ B 
(
A',B':T List. C = (A' @ B') & A' A & B' B)L:T List. L nil L = nilL:T List. nil L Truex1,x2:T, L1,L2:T List. [x1 / L1] [x2 / L2] x1 = x2 & L1 L2 
[x1 / L1] L2| Rank | Theorem | Name |
| 4 | Thm* C,A,B:T List. C A @ B (A',B':T List. C = (A' @ B') & A' A & B' B) | [sublist_append_iff] |
| cites | ||
| 3 | Thm* L:T List. L nil L = nil | [sublist_nil] |
| 0 | Thm* L:T List. nil L True | [nil_sublist] |
| 1 | Thm* x1,x2:T, L1,L2:T List. [x1 / L1] [x2 / L2] x1 = x2 & L1 L2 [x1 / L1] L2 | [cons_sublist_cons] |