forall (P: N -> Type), P 0 -> (forall n, P n -> P (1 + n)) -> forall n, P n. Proof. pose (Q := fun s : SemiRings.Operations => forall P : s -> Type, P 0 -> (forall n, P n -> P (1 + n)) -> forall n, P n). change (Q (SemiRings.BuildOperations N)). apply (from_nat_stmt nat). unfold Q;clear Q. simpl. exact nat_induction. Qed.
Require Import Require Import Import SemiRings.