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