`{Integers Z} `{IsCRing R} (f: Z -> R) {h: IsSemiRingPreserving f} x : f x = integers_to_ring Z R x. Proof. symmetry. apply integers_initial. Qed.
Require Import Require Import Import NatPair.Instances.