(P : forall n : nat, Fin n -> Type) (z : forall n : nat, P n.+1 fin_zero) (s : forall (n : nat) (k : Fin n), P n k -> P n.+1 (fsucc k)) {n : nat} (k : Fin n) : P n k. Proof. refine (transport (P n) (path_fin_to_finnat_to_fin k) _). refine (finnat_ind (fun n u => P n (finnat_to_fin u)) _ _ _). - intro. apply z. - intros n' u c. refine ((path_finnat_to_fin_succ _)^ # _). by apply s. Defined.
Require Import