proposition: Lemma outputs_m_revert_trace : forall tr, no_output_at_backup_trace tr -> outputs_m tr = outputs_1 (revert_trace tr).
proof: Proof. Proof using. unfold outputs_1. induction tr; simpl; intros. - auto. - repeat break_match; subst. + eauto using NOABT_tail. + rewrite IHtr by eauto using NOABT_tail. rewrite map_app. rewrite map_of_filterMap. f_equal. apply filterMap_ext. intros. repeat break_match; auto. + rewrite IHtr by eauto using NOABT_tail. auto. + find_copy_apply_lem_hyp NOABT_tail. find_apply_lem_hyp NOABT_contra. intuition; break_exists; subst; simpl; auto. Qed.
imports: Verdi(Verdi HandlerMonad)