fact: Definition inductive (step : step_relation) (P : A -> Prop) := forall (a a': A) (os : list trace), P a -> step a a' os -> P a'.
imports: Coq(List) StructTact(StructTactics) StructTact(Update Update2 RemoveAll) Coq(Sumbool Relation_Definitions RelationClasses) Cheerios(Cheerios)