proposition: Theorem true_in_reachable_reqs : forall (step : step_relation) init (P : A -> Prop), (P init) -> (forall a a' out, step a a' out -> reachable step init a -> P a -> P a') -> true_in_reachable step init P.
proof: Proof. Proof using. intros. unfold true_in_reachable, reachable in *. intros. break_exists. match goal with H : refl_trans_1n_trace _ _ _ _ |- _ => induction H end; intuition eauto. match goal with H : P _ -> _ |- _ => apply H end; intros; break_exists; match goal with H : forall _ _ _, step _ _ _ -> _ |- _ => eapply H end; eauto; eexists; econstructor; eauto. Qed.
imports: Coq(List) StructTact(StructTactics) StructTact(Update Update2 RemoveAll) Coq(Sumbool Relation_Definitions RelationClasses) Cheerios(Cheerios)