proposition: Lemma last_Some l x : last l = Some x ↔ ∃ l', l = l' ++ [x].
proof: Proof. split. - destruct l as [|x' l'] using rev_ind; [done|]. rewrite last_snoc. naive_solver. - intros [l' ->]. by rewrite last_snoc. Qed.
imports: stdpp(options)