proposition: Corollary add_hom x y : iμ (x + y) = iμ x i⊕ iμ y.
proof: Proof. Proof using ext_model FA_model. induction x. - now rewrite add_zero. - change (iσ iμ (x + y) = iσ iμ x i⊕ iμ y). now rewrite add_rec, IHx. Qed.
imports: Undecidability.FOL.Arithmetics(FA Signature) Undecidability.FOL(PA) Lia List Vector