proposition: Lemma processInputs_cons_defn : forall (st : @data base_params) (x : @input base_params) l, processInputs st (x :: l) = let (os, d') := handler x st in let (d'', os') := processInputs d' l in (d'', os :: os').
proof: Proof. Proof using. auto. Qed.
imports: Verdi(Verdi HandlerMonad)