proposition: Lemma processInputs_app : forall l1 l2 d, processInputs d (l1 ++ l2) = let (d', os) := processInputs d l1 in let (d'', os') := processInputs d' l2 in (d'', os ++ os').
proof: Proof. Proof using. induction l1; intros; simpl in *; repeat break_match. - auto. - find_inversion. find_higher_order_rewrite. repeat break_match. repeat find_inversion. repeat find_rewrite. find_inversion. auto. Qed.
imports: Verdi(Verdi HandlerMonad)