[STATEMENT]
lemma rfoldl_simps[simp]: 
    "rfoldl f s [] = RETURN s"
    "rfoldl f s (x#ls) = do { s\<leftarrow>f s x; rfoldl f s ls}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rfoldl f s [] = RETURN s &&& rfoldl f s (x # ls) = f s x \<bind> (\<lambda>s. rfoldl f s ls)
[PROOF STEP]
apply (subst rfoldl.simps, simp)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done