proposition: Fact nat_is_PA_model : forall ax rho, PA ax -> sat interp_nat rho ax.
proof: Proof. intros rho psi []. repeat (destruct H as [<- | H]; auto). all: cbn; try congruence. inversion H. apply nat_induction. Qed.
imports: Undecidability.FOL.Arithmetics(FA Signature) Undecidability.FOL(PA) Lia List Vector