proposition: Corollary mult_nat_to_model : forall z x y, 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 <- mult_hom, H. Qed.
imports: Undecidability.FOL.Arithmetics(FA Signature) Undecidability.FOL(PA) Lia List Vector