proposition: Lemma inputs_1_invert_app : forall tr tr' x, inputs_1 tr = tr' ++ [x] -> exists y z, tr = y ++ [z] /\ inputs_1 y = tr' /\ inputs_1 [z] = [x].
proof: Proof. Proof using. intros tr. pose proof list_destruct_last _ tr. intuition. - subst. destruct tr'; discriminate. - break_exists. subst. rewrite inputs_1_app in *. simpl in *. find_apply_lem_hyp app_inj_tail. intuition eauto. Qed.
imports: Verdi(Verdi HandlerMonad)