(P : Pos -> Type) (a : P 1) (f : forall p, P p -> P (pos_succ p)) (p : Pos) : pos_peano_ind P a f (pos_succ p) = f _ (pos_peano_ind P a f p). Proof. revert P a f. induction p; trivial. intros P a f. srapply IHp. Qed.
Require Import Basics.Overture Basics.Tactics Basics.Decidable