proposition: Lemma revert_trace_app : forall tr1 tr2, revert_trace (tr1 ++ tr2) = revert_trace tr1 ++ revert_trace tr2.
proof: Proof. Proof using. induction tr1; intros; simpl. - auto. - rewrite IHtr1. repeat break_match; subst. + auto. + rewrite <- app_assoc. auto. Qed.
imports: Verdi(Verdi HandlerMonad)