proposition: Lemma list_destruct_last : forall A (l : list A), l = [] \/ exists l' x, l = l' ++ [x].
proof: Proof. Proof using. induction l; intuition. - subst. right. exists nil. simpl. eauto. - break_exists. subst. right. eexists. eexists. rewrite app_comm_cons. eauto. Qed.
imports: Verdi(Verdi HandlerMonad)