// Complete this proof following the mechanical strategy of repeatedly expanding
// "assume"s.
lemma s1()
  ensures forall x: nat :: x % 2 == 0 ==> exists y: nat :: x == 2 * y
{
  assume forall x: nat :: x % 2 == 0 ==> exists y: nat :: x == 2 * y;
}
// Note that Dafny accepts this "proof," but it's bogus because an "assume"
// remains.  Refine it until there is no "assume" left.