proposition: Lemma pow_plus k1 k2 x y z : pow k1 x y -> pow k2 y z -> pow (k1 + k2) x z.
proof: Proof. induction 1; cbn; eauto using pow. Qed.
imports: Undecidability.Shared.Libs.PSL.Base Undecidability.Shared.Libs.PSL.Vectors.Vectors