(P : Type) (a : P) (f : Pos -> P -> P) (p : Pos) : pos_peano_rec P a f (pos_succ p) = f p (pos_peano_rec P a f p) := pos_peano_ind_beta_pos_succ (fun _ => P) a f p.
Require Import Basics.Overture Basics.Tactics Basics.Decidable