import Init

def OA_statement : Prop := (∀ (State Op : Type) (step : Op → State → Option State) (xs ys : List Op) (s : State),
 (xs ++ ys).foldl (fun prior op => prior.bind (step op)) (some s) =
 ys.foldl (fun prior op => prior.bind (step op))
   (xs.foldl (fun prior op => prior.bind (step op)) (some s)))

theorem OA_target : OA_statement :=
  by
    intro State Op step xs ys s
    exact List.foldl_append

#print axioms OA_target
#check OA_target