fact: Definition step_failure_disk_ops_star : step_relation (list do_name * do_network) (do_name * (input + list output)) := refl_trans_1n_trace step_failure_disk_ops.
imports: Coq(List) StructTact(StructTactics) StructTact(Update Update2 RemoveAll) Coq(Sumbool Relation_Definitions RelationClasses) Cheerios(Cheerios)