proposition: Lemma star_pow x y : star x y <-> exists n, pow n x y.
proof: Proof. split. - induction 1; firstorder eauto using pow. - intros (n&H). induction H; eauto using star. Qed.
imports: Undecidability.Shared.Libs.PSL.Base Undecidability.Shared.Libs.PSL.Vectors.Vectors