proposition: Fact nat_eval_num (sigma : env nat) n : @eval _ _ _ interp_nat sigma (μ n) = n.
proof: Proof. induction n. - reflexivity. - cbn. now rewrite IHn. Qed.
imports: Undecidability.FOL.Arithmetics(FA Signature) Undecidability.FOL(PA) Lia List Vector