proposition: Lemma nat_sat_Fr_Q P : (extend_interp interp_nat P) ⊫= Fr_ Qeq.
proof: Proof. intros ρ a Qa. repeat (destruct Qa as [<-|Qa]). all: cbn -[FAeq]; try refine (fun A => let F := A _ rho in _); intuition. - apply H. intros ->. apply H0. intros ->. auto. - now apply H. - destruct d; eauto. - destruct Qa. Qed.
imports: List Lia Undecidability(Shared.ListAutomation) Undecidability.FOL(FullSyntax) Undecidability.FOL.Arithmetics(Robinson NatModel)