proposition: Lemma nat_is_FA_model : forall rho phi, List.In phi FAeq -> sat interp_nat rho phi.
proof: Proof. intros rho phi. intros H. repeat (destruct H as [<- | H]; auto). all: cbn; try congruence. inversion H. Qed.
imports: Undecidability.FOL.Arithmetics(FA Signature) Undecidability.FOL(PA) Lia List Vector