datatype List<T> = Nil | Cons(head: T, tail: List<T>)

type IntList = List<int>

function Count<X(==)>(xs: List<X>, val: X): nat {
  match xs
  case Nil => 0
  case Cons(x, tail) => (if val == x then 1 else 0) + Count(tail, val)
}

function InsertionSort(xs: IntList): IntList {
  match xs
  case Nil => Nil
  case Cons(x, tail) =>
    var sortedTail := InsertionSort(tail);
    Insert(x, sortedTail)
}

function Insert(x: int, xs: IntList): IntList {
  match xs
  case Nil => Cons(x, Nil)
  case Cons(y, tail) =>
    if x <= y then Cons(x, xs) else Cons(y, Insert(x, tail))
}

lemma InsertionSortPreservesCounts(xs: IntList, val: int)
  ensures Count(xs, val) == Count(InsertionSort(xs), val)
{
  match xs
  case Nil =>
  case Cons(x, tail) =>
    var sortedTail := InsertionSort(tail);
    var result := Insert(x, sortedTail);
    assert result == InsertionSort(xs);

    // Complete this case of the proof...

}

// ... perhaps with the help of a lemma about Insert and Count