(h : nat -> R) `{!IsSemiRingPreserving h} x : naturals_to_semiring nat R x = h x. Proof. induction x as [|n E]. + change (0 = h 0). apply symmetry,preserves_0. + rewrite f_S. change (1 + naturals_to_semiring nat R n = h (1+n)). rewrite (preserves_plus (f:=h)). rewrite E. apply ap10,ap,symmetry,preserves_1. Qed.
Require Import