(B : nat -> Type) (z : forall n : nat, B n.+1) (s : forall (n : nat) (k : Fin n), B n -> B n.+1) (n : nat) : fin_rec B z s fin_zero = z n. Proof. apply (fin_ind_beta_zero (fun n _ => B n)). Defined.
Require Import