by
  intro State Op step xs ys s
  exact List.foldl_append