proposition: Lemma from_nat_stmt: ∀ (s: Statement varieties.semirings.theory) (w : Vars varieties.semirings.theory (varieties.semirings.object N) nat), (∀ v: Vars varieties.semirings.theory (varieties.semirings.object nat) nat, eval_stmt varieties.semirings.theory v s) → eval_stmt varieties.semirings.theory w s.
proof: Proof. pose proof (@naturals_initial nat _ _ _ _ _ _ _) as AI. pose proof (@naturals_initial N _ _ _ _ _ _ _) as BI. intros s w ?. apply (transfer_statement _ (@categories.initials_unique' semirings.Object _ _ _ _ _ (semirings.object nat) (semirings.object N) _ AI _ BI)). intuition. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.implementations.peano_naturals MathClasses.theory.rings Coq.Arith.PeanoNat MathClasses.categories.varieties MathClasses.theory.ua_transference MathClasses.interfaces.naturals