proposition: Lemma sat_Qeq : (forall ax, List.In ax Qeq -> ⊨ ax).
proof: Proof. Proof using axioms. intros x [<- |[<- |[<- |[<- |[<- |[<- |[<- |[<- |[<- |[<- |[<- |[<- |[<- |[]]]]]]]]]]]]]]. 1-10: apply axioms; apply PAeq_FA; cbn; eauto 15; fail. - apply axioms. apply PAeq_discr. - apply axioms. apply PAeq_inj. - intros ρ d. unfold ax_cases. evar (phi : form). specialize (axioms (PAeq_induction phi)) as Hax. cbn in Hax. apply Hax. + cbn. left. specialize (@axioms (∀ $0 == $0)). unshelve eapply axioms. 1:easy. apply PAeq_FA; cbn; eauto 15. + intros dd _. cbn. right. exists dd. specialize (@axioms (∀ $0 == $0)). unshelve eapply axioms. 1:easy. apply PAeq_FA; cbn; eauto 15. Qed.
imports: Undecidability.FOL.Arithmetics(FA Signature) Undecidability.FOL(PA) Lia List Vector