fact: Definition reachable step init a := exists out, refl_trans_1n_trace step init a out.
imports: Coq(List) StructTact(StructTactics) StructTact(Update Update2 RemoveAll) Coq(Sumbool Relation_Definitions RelationClasses) Cheerios(Cheerios)