proposition: Lemma nat_is_Q_model : forall rho phi, List.In phi Qeq -> sat interp_nat rho phi.
proof: Proof. intros rho phi. intros H. repeat (destruct H as [<- | H]; auto). all: cbn; try congruence. 2: inversion H. induction d. now left. right. destruct IHd. exists 0. congruence. exists d. reflexivity. Qed.
imports: Undecidability.FOL.Arithmetics(FA Signature) Undecidability.FOL(PA) Lia List Vector