(P : Pos -> Type) (a : P 1) (f : forall p, P p -> P (pos_succ p)) (p : Pos) : P p := let f2 := (fun p => P (p~0)) (f _ a) (fun p (x : P p~0) => f _ (f _ x)) in match p with | q~1 => f _ (f2 q) | q~0 => f2 q | 1 => a end.
Require Import Basics.Overture Basics.Tactics Basics.Decidable