Here are some answers for the exercises.

1. To prove: x `elem` (xs ++ ys) = (x `elem` xs) || (x `elem` ys), for all x,xs,ys.

Proof: by structural induction.

Let P(xs) = "∀x,ys . x `elem` (xs ++ ys) = (x `elem` xs) || (x `elem` ys)".

base case: P([]) = "forall x, ys . x `elem` ([] ++ ys) = (x `elem` []) || (x `elem` ys)".

x `elem` ([] ++ ys)
= x `elem` ys		-- defn. ++
= False || x `elem` ys		-- defn. ||
= (x `elem` []) || x `elem` ys		-- defn. elem

step case: P(as) => P(a:as).
assume: P(as) = "forall x, ys . x `elem` (as ++ ys) = (x `elem` as) || (x `elem` ys)" (I.H.)
show: P(a:as) = "forall x, ys . x `elem` ((a:as) ++ ys) = (x `elem` (a:as)) || (x `elem` ys)"

x `elem` ((a:as) ++ ys)
= x `elem` (a : (as ++ ys)		-- defn. ++
= x == a || (x `elem` (as ++ ys))		-- defn. elem
= x == a || ((x `elem` as) || (x `elem` ys))		-- I.H.
= (x == a || (x `elem` as)) || (x `elem` ys)		-- || is associative
= (x `elem` (a:as)) || (x `elem` ys)		-- defn. elem

Which is what we had to prove.

2. To prove: length (rev xs) = length xs, for all xs.

Proof: by structural induction.

Let P(xs) = "length (rev xs) = length xs".

base case: P([]) = "length (rev []) = length []".

length (rev [])
= length []		-- defn. rev

step case: P(as) => P(a:as).
assume: P(as) = "length (rev as) = length as" (I.H.)
show: P(a:as) = "length (rev (a:as)) = length (a:as)"

length (rev (a:as))
= length (rev as ++ [a])		-- defn. rev
= length (rev as) + length [a]		-- length/++ lemma
= length as + length [a]		-- I.H.
= length as + 1		-- defn. length
= 1 + length as		-- + commutative
= length (a:as)		-- defn. length

Which is what we had to prove.

3. To prove: x `elem` rev xs = x `elem` xs, for all x,xs.

Proof: by structural induction.

Let P(xs) = "∀x . x `elem` rev xs = x `elem` xs"

base case: P([]) = "∀x . x `elem` rev [] = x `elem` []".

x `elem` rev []
= x `elem` []		-- defn. rev

step case: P(as) => P(a:as).
assume: P(as) = "∀x . x `elem` rev as = x `elem` as" (I.H.)
show: P(a:as) = "∀x . x `elem` rev (a:as) = x `elem` (a:as)"

x `elem` rev (a:as)
= x `elem` (rev as ++ [a])		-- defn. rev
= (x `elem` rev as) || (x `elem` [a])		-- exercise 1.
= (x `elem` as) || (x `elem` [a])		-- I.H.
= (x `elem` [a]) || (x `elem` as)		-- || commutative
= x == a || (x `elem` as)		-- defn. elem
= x `elem` (a:as)		-- defn. elem

Which is what we had to prove.

4. To prove: x `elem` xs ==> length xs > 0, for all x,xs

Proof: by case split on xs.

case 1: xs = [].

x `elem` xs ==> length xs > 0
= x `elem` [] ==> length [] > 0		-- xs = []
= False ==> length [] > 0		-- defn. elem
= True		-- basic logic

case 2: xs = a:as.

x `elem` xs ==> length xs > 0
= x `elem` (a:as) ==> length (a:as) > 0		-- xs = a:as
= x `elem` (a:as) ==> (1 + length as) > 0		-- defn. length
= x `elem` (a:as) ==> True		-- basic arithmetic, length as >= 0
= True		-- basic logic

Which is what we had to prove.

5. To prove: take (length xs) xs = xs, for all xs.

Proof: by structural induction.

Let P(xs) = "take (length xs) xs = xs".

base case: P([]) = "take (length []) [] = []".

take (length []) []
= take 0 []		-- defn. length
= []		-- defn. take

step case: P(as) => P(a:as).
assume: P(as) = "take (length as) as = as" (I.H.)
show: P(a:as) = "take (length (a:as)) (a:as) = a:as"

take (length (a:as)) (a:as)
= take (1 + length as) (a:as)		-- defn. length
= a : take (1 + length as - 1) as		-- defn. take, length as >= 0
= a : take (length as) as		-- basic arithmetic
= a : as		-- I.H.

Which is what we had to prove.

6. To prove: even x = not (odd x), for all x.

Proof: by structural induction.

Let P(x) = "even x = not (odd x)".

base case: P(Zero) = "even Zero = not (odd Zero)".

even Zero
= True		-- defn. even
= not False		-- defn. not
= not (odd Zero)		-- defn. odd

step case: P(a) => P(Succ a).
assume: P(a) = "even a = not (odd a)" (I.H.)
show: P(Succ a) = "even (Succ a) = not (odd (Succ a))"

even (Succ a)
= not (even a)		-- defn. even
= not (not (odd a))		-- I.H.
= odd a		-- basic logic (not (not x) = x)
= not (odd (Succ a))		-- defn. odd

Which is what we had to prove.

7. To prove: plus x Zero = x, for all x.

Proof: by structural induction.

Let P(x) = "plus x Zero = x".

base case: P(Zero) = "plus Zero Zero = Zero".

plus Zero Zero
= Zero		-- defn. plus

step case: P(a) => P(Succ a).
assume: P(a) = "plus a Zero = a" (I.H.)
show: P(Succ a) = "plus (Succ a) Zero = (Succ a)"

plus (Succ a) Zero
= Succ (plus a Zero)		-- defn. plus
= Succ a		-- I.H.

Which is what we had to prove.

8. To prove: even (plus x x), for all x.

Proof: by structural induction.

Let P(x) = "even (plus x x)".

base case: P(Zero) = "even (plus Zero Zero)".

even (plus Zero Zero)
= even Zero		-- defn. plus
= True		-- defn. even

step case: P(a) => P(Succ a).
assume: P(a) = "even (plus a a)" (I.H.)
show: P(Succ a) = "even (plus (Succ a) (Succ a))"

even (plus (Succ a) (Succ a))
= even (Succ (plus a (Succ a)))		-- defn. plus
= not (even (plus a (Succ a)))		-- defn. even
= not (even (Succ (plus a a)))		-- helper lemma (see below)
= not (not (even (plus a a)))		-- defn. even
= even (plus a a)		-- basic logic (not (not x) = x)
= True		-- I.H.

Which is what we had to prove.

We also need to prove the helper lemma:

To prove: plus x (Succ y) = Succ (plus x y), for all x,y.

Proof: by structural induction.

Let P(x) = "∀y. plus x (Succ y) = Succ (plus x y)":

base case: P(Zero) = "∀y. plus Zero (Succ y) = Succ (plus Zero y)".

plus Zero (Succ y)
= Succ y		-- defn. plus
= Succ (plus Zero y)		-- defn. plus

step case: P(a) => P(a:as).
assume: P(a) = "∀y. plus a (Succ y) = Succ (plus a y)" (I.H.)
show: P(Succ a) = "∀y. plus (Succ a) (Succ y) = Succ (plus (Succ a) y)"

plus (Succ a) (Succ y)
= Succ (plus a (Succ y))		-- defn. plus
= Succ (Succ (plus a y))		-- I.H.
= Succ (plus (Succ a) y)		-- defn. plus

Which is what we had to prove.

9. To prove: size p = length (flatten p), for all p.

Proof: by structural induction.

Let P(p) = "size p = length (flatten p)".

base case: P(Empty) = "size Empty = length (flatten Empty)".

size Empty
= 0		-- defn. size
= length []		-- defn. length
= length (flatten Empty)		-- defn. flatten

step case: ( P(v) /\ P(w) ) => P(Node a v w).
assume: P(v) = "size v = length (flatten v)"
    and   P(w) = "size w = length (flatten w)" (I.H.)
show: P(Node a v w) = "size (Node a v w) = length (flatten (Node a v w))"

size (Node a v w)
= 1 + size v + size w		-- defn. size
= 1 + length (flatten v) + length (flatten w)		-- I.H. * 2
= length (flatten v ++ [a] ++ flatten w)		-- length/++ lemma * 2
= length (flatten (Node a v w))		-- defn. flatten

Which is what we had to prove.

10. To prove: flatten (swap p) = rev (flatten p), for all p.

Proof: by structural induction.

Let P(p) = "flatten (swap p) = rev (flatten p)".

base case: P(Empty) = "flatten (swap Empty) = rev (flatten Empty)".

flatten (swap Empty)
= flatten Empty		-- defn. swap
= []		-- defn. flatten
= rev []		-- defn. rev
= rev (flatten Empty)		-- defn. flatten

step case: ( P(v) /\ P(w) ) => P(Node a v w).
assume: P(v) = "flatten (swap v) = rev (flatten v)"
    and   P(w) = "flatten (swap w) = rev (flatten w)" (I.H.)
show: P(Node a v w) = "flatten (swap (Node a v w)) = rev (flatten (Node a v w))"

flatten (swap (Node a v w))
= flatten (Node a (swap w) (swap v))		-- defn. swap
= flatten (swap w) ++ [a] ++ flatten (swap v)		-- defn. flatten
= rev (flatten w) ++ [a] ++ rev (flatten v)		-- I.H. * 2
= rev (flatten w) ++ rev [a] ++ rev (flatten v)		-- defn. rev
= rev ([a] ++ flatten w) ++ rev (flatten v)		-- rev/++ lemma
= rev (flatten v ++ [a] ++ flatten w)		-- rev/++ lemma
= rev (flatten (Node a v w))		-- defn. flatten

Which is what we had to prove.