proposition: Lemma num_add_homomorphism x y : Gamma ⊢ ( num x ⊕ num y == num (x + y) ).
proof: Proof. Proof using G. induction x; cbn. - apply (@AllE _ _ _ _ _ _ (zero ⊕ $0 == $0) ). apply Weak with FAeq. apply Ctx;firstorder. assumption. - eapply transitivity. apply Add_rec. now apply eq_succ. Qed.
imports: Undecidability.FOL.Arithmetics(FA Signature) Undecidability.FOL(PA) Lia List Vector