proposition: Lemma num_bound n k : bounded_t k (num n).
proof: Proof. induction n; cbn; constructor. - intros t H. inversion H. - intros t [-> | H]%vec_cons_inv; [easy | inversion H]. Qed.
imports: Undecidability.FOL.Arithmetics.Signature List