Structural induction proof

Question

I need to prove the following:

reverse(append(zs, z)) = Cons(z, reverse(zs))

Where:

sealed abstract class IntList
case object Nil extends IntList
case class Cons(x: Int, xs: IntList) extends IntList

def append(xs: IntList, x: Int): IntList = xs match {
    case Nil => Cons(x, Nil)
    case Cons(y, ys) => Cons(y, append(ys, x))
} 

def reverse(xs: IntList): IntList = xs match {
    case Nil => Nil
    case Cons(x, ys) => append(reverse(ys), x)
}

I've already made the induction basis:

Assume $zs=Nil$. \begin{align*} reverse(append(zs, z)) &=reverse(append(Nil,z)) \\ &=reverse(Cons(z,Nil)) \\ &=append(reverse(Cons(Nil),z)) \\ &=Cons(z,reverse(Nil)) \end{align*}

How do I make the induction step?

Answer 1

Here is the complete proof:

reverse(append(Cons(w,ws),z)) = reverse(Cons(w,append(ws,z))) = append(reverse(append(ws,z)),w) = append(Cons(z,reverse(ws)),w) = Cons(z,append(reverse(ws),w)) = Cons(z,reverse(Cons(w,ws)))

At one point we used the inductive hypothesis.