proposition: Theorem true_in_reachable_elim : forall (step : step_relation) init (P : A -> Prop), true_in_reachable step init P -> (P init) /\ (forall a a' out, step a a' out -> reachable step init a -> P a -> P a').
proof: Proof. Proof using. intros. unfold true_in_reachable, reachable in *. intros. intuition. - apply H; eexists; econstructor. - apply H. break_exists. eexists. apply refl_trans_n1_1n_trace. find_apply_lem_hyp refl_trans_1n_n1_trace. econstructor; eauto. Qed.
imports: Coq(List) StructTact(StructTactics) StructTact(Update Update2 RemoveAll) Coq(Sumbool Relation_Definitions RelationClasses) Cheerios(Cheerios)