proposition: Lemma compute_fin_rec_fsucc (B : nat -> Type) (z : forall n : nat, B n.+1) (s : forall (n : nat) (k : Fin n), B n -> B n.+1) {n : nat} (k : Fin n) : fin_rec B z s (fsucc k) = s n k (fin_rec B z s k).
proof: Proof. apply (compute_fin_ind_fsucc (fun n _ => B n)). Defined.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Spaces.Nat.Core HoTT.Spaces.Finite.FinNat HoTT.Spaces.Finite.Fin