proposition: Theorem step_star_inductive : forall step P, inductive step P -> forall (a : A) a' os, P a -> (refl_trans_1n_trace step) a a' os -> P a'.
proof: Proof. Proof using. unfold inductive. intros. induction H1; auto. forwards; eauto. Qed.
imports: Coq(List) StructTact(StructTactics) StructTact(Update Update2 RemoveAll) Coq(Sumbool Relation_Definitions RelationClasses) Cheerios(Cheerios)