Require Import sepcomp.StructuredInjections.
Require Import sepcomp.effect_simulations.

Import SM_simulation.

Arguments core_diagram : default implicits.
Arguments match_sm_wd : default implicits.
Arguments core_at_external : default implicits.
Arguments disjoint_extern_local_Src : default implicits.