proposition: Lemma star_pow R x y : star R x y <-> exists n, pow R n x y.
proof: Proof. split; intros A. - induction A as [|x x' y B _ [n IH]]. + exists 0. reflexivity. + exists (S n), x'. auto. - destruct A as [n A]. revert x A. induction n; intros x A. + destruct A. constructor. + destruct A as [x' [A B]]. econstructor; eauto. Qed.
imports: Undecidability.Shared.Libs.PSL.Base Lia Arith Arith