proposition: Lemma star_simpl_ind R (p : X -> Prop) y : p y -> (forall x x', R x x' -> star R x' y -> p x' -> p x) -> forall x, star R x y -> p x.
proof: Proof. intros A B. induction 1; eauto. Qed.
imports: Undecidability.Shared.Libs.PSL.Base Lia Arith Arith