proposition: Lemma inputs_1_singleton : forall l i, inputs_1 l = [i] -> exists os, l = [(i, os)].
proof: Proof. Proof using. intros. destruct l; simpl in *. - discriminate. - find_inversion. find_apply_lem_hyp inputs_1_nil_is_nil. subst. destruct p. eauto. Qed.
imports: Verdi(Verdi HandlerMonad)