proposition: Lemma correspond_preserved_primary_same_no_outputs : forall sigma sigma' st tr_1 tr_m tr_m', correspond st sigma tr_1 tr_m -> sigma' Primary = sigma Primary -> outputs_m tr_m' = [] -> correspond st sigma' tr_1 (tr_m ++ tr_m').
proof: Proof. Proof using. unfold correspond. intros. rewrite outputs_m_app. repeat find_rewrite. rewrite app_nil_r. auto. Qed.
imports: Verdi(Verdi HandlerMonad)