proposition: Corollary add_nat_to_model : forall x y z, x + y = z -> (iμ x i⊕ iμ y = iμ z).
proof: Proof. Proof using ext_model FA_model. intros x y z H. now rewrite <- add_hom, H. Qed.
imports: Undecidability.FOL.Arithmetics(FA Signature) Undecidability.FOL(PA) Lia List Vector