proposition: Lemma correspond_preserved_snoc : forall sigma tr_1 tr_m st sigma' st' i l, correspond st sigma tr_1 tr_m -> handler i st = (l, st') -> state (sigma' Primary) = state (sigma Primary) -> queue (sigma' Primary) = queue (sigma Primary) ++ [i] -> correspond st' sigma' (tr_1 ++ [(i,l)]) (tr_m ++ [(Primary, inl (Request i))]).
proof: Proof. Proof using. unfold correspond. intros. rewrite outputs_m_app, outputs_1_app in *. repeat break_match. rewrite <- app_assoc. simpl. repeat find_rewrite. rewrite processInputs_app in *. repeat break_match. repeat tuple_inversion. simpl in *. break_match. tuple_inversion. break_and. subst. find_rewrite. tuple_inversion. rewrite app_assoc. find_rewrite. auto. Qed.
imports: Verdi(Verdi HandlerMonad)