Structural induction proof 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 =&gt; Cons(x, Nil)
    case Cons(y, ys) =&gt; Cons(y, append(ys, x))
} 

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


I've already made the induction basis:

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

How do I make the induction step?
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.