fact: Definition step_ordered_dynamic_init : ordered_dynamic_network := mkODNetwork [] (fun _ _ => []) (fun _ => None).
imports: Coq(List) StructTact(StructTactics) StructTact(Update Update2 RemoveAll) Coq(Sumbool Relation_Definitions RelationClasses) Cheerios(Cheerios)