fact: Definition true_in_reachable step init (P : A -> Prop) := forall a, reachable step init a -> P a.
imports: Coq(List) StructTact(StructTactics) StructTact(Update Update2 RemoveAll) Coq(Sumbool Relation_Definitions RelationClasses) Cheerios(Cheerios)