proposition: Lemma correspond_preserved_primary_apply_entry : forall sigma sigma' st tr_1 tr_m tr_m' i l d h, correspond st sigma tr_1 tr_m -> handler i (state (sigma h)) = (l, state d) -> sigma' Primary = d -> outputs_m tr_m' = [l] -> h = Primary -> queue (sigma h) = i :: queue d -> correspond st sigma' tr_1 (tr_m ++ tr_m').
proof: Proof. Proof using. unfold correspond. intros. subst. rewrite outputs_m_app. repeat find_rewrite. simpl in *. repeat break_match. repeat find_inversion. find_rewrite. find_inversion. rewrite <- app_assoc. auto. Qed.
imports: Verdi(Verdi HandlerMonad)