proposition: Lemma num_mult_homomorphism (x y : nat) : Gamma ⊢ ( num x ⊗ num y == num (x * y) ).
proof: Proof. Proof using G. induction x; cbn. - apply (@AllE _ _ _ _ _ _ (zero ⊗ $0 == zero)). apply Weak with FAeq. apply Ctx; firstorder. assumption. - eapply transitivity. apply Mult_rec. eapply transitivity. 2: apply num_add_homomorphism. apply eq_add. apply reflexivity. apply IHx. Qed.
imports: Undecidability.FOL.Arithmetics(FA Signature) Undecidability.FOL(PA) Lia List Vector