#### Sub-lists

I have used this exercise as a good one for getting a student up to speed with a proof-assistant such as HOL4.

Using your theorem-proving system of choice, define the notion of *sublist*, a binary relation on lists *l _{1}* and

*l*, which is true if and only if all the elements of

_{2}*l*appear in

_{1}*l*in the same order. Naturally,

_{2}*l*may contain other elements.

_{2} For example, `[1,2,3]`

is a sub-list of `[0,1,2,2,4,5,6,3,10]`

, but is not a sub-list of `[1,4,3,2]`

.

Having defined this relation in whatever way seems most natural, prove that it is reflexive, anti-symmetric and transitive.