fact: Definition step_ordered_failure_init : list name * ordered_network := ([], step_ordered_init).
imports: Coq(List) StructTact(StructTactics) StructTact(Update Update2 RemoveAll) Coq(Sumbool Relation_Definitions RelationClasses) Cheerios(Cheerios)