// Code from last class

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

// New definitions from this class

function Map<A, B>(f: A -> B, ls: List<A>): List<B> {
  match ls
  case Nil => Nil
  case Cons(x, ls') => Cons(f(x), Map(f, ls'))
}

function Foldl<A, B>(f : (A, B) -> B, acc: B, ls: List<A>): B {
  match ls
  case Nil => acc
  case Cons(x, ls') => Foldl(f, f(x, acc), ls')
}

// Your task: fill in a proof for this lemma

lemma FoldlMap<A, B, C>(f: A -> B, g : (B, C) -> C, acc: C, ls: List<A>)
  ensures Foldl(g, acc, Map(f, ls)) == Foldl((x, a) => g(f(x), a), acc, ls)