lemma DropSame(xs: List, n: nat)
  requires n <= Length(xs)
  ensures Drop(xs, n) == Drop'(xs, n)
{
  if n < 2 {
    // easy
  } else {

  }
}

// Here are the definitions lifted from the code we just went through.
  
datatype List<X> = Nil | Cons(head: X, tail: List<X>)

function Length(xs: List): nat {
  if xs == Nil then 0 else 1 + Length(xs.tail)
}

function Drop(xs: List, n: nat): List
  requires n <= Length(xs)
{
  if n == 0 then xs else Drop(xs.tail, n - 1)
}

function Drop'(xs: List, n: nat): (r: List)
  requires n <= Length(xs)
  ensures Length(r) == Length(xs) - n
{
  // To take the `.tail` of `Drop'(xs, n - 1)` in the following line, we need
  // to know that this call returns a nonempty list. To obtain that piece of
  // information, we add a postcondition of `Drop'` that speaks about the length
  // of its result.
  if n == 0 then xs else Drop'(xs, n - 1).tail
}