Require Import
  HoTT.Basics
  HoTT.Types
  HoTT.Universes.HSet
  HoTT.Spaces.Nat.Core
  HoTT.Spaces.Finite.FinNat
  HoTT.Spaces.Finite.Fin.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Local Open Scope nat_scope.

Definition fin_ind (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.
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.
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
  refine (transport (P n) (path_fin_to_finnat_to_fin k) _).
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 (finnat_to_fin (fin_to_finnat k))
  refine (finnat_ind (fun n u => P n (finnat_to_fin u)) _ _ _).
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
forall n : nat, P n.+1 (finnat_to_fin (zero_finnat n))
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
forall (n : nat) (u : FinNat n),
P n (finnat_to_fin u) ->
P n.+1 (finnat_to_fin (succ_finnat u))
  -
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
forall n : nat, P n.+1 (finnat_to_fin (zero_finnat n)) intro.
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
n0: nat
P n0.+1 (finnat_to_fin (zero_finnat n0)) apply z.
  -
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
forall (n : nat) (u : FinNat n),
P n (finnat_to_fin u) ->
P n.+1 (finnat_to_fin (succ_finnat u)) intros n' u c.
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
n': nat
u: FinNat n'
c: P n' (finnat_to_fin u)
P n'.+1 (finnat_to_fin (succ_finnat u))
    refine ((path_finnat_to_fin_succ _)^ # _).
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
n': nat
u: FinNat n'
c: P n' (finnat_to_fin u)
P n'.+1 (fsucc (finnat_to_fin u))
    by apply s.
Defined.

Lemma fin_ind_beta_zero (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)
  : fin_ind P z s fin_zero = z n.
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
fin_ind P z s fin_zero = z n
Proof.
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
fin_ind P z s fin_zero = z n
  unfold fin_ind.
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
transport (P n.+1)
  (path_fin_to_finnat_to_fin fin_zero)
  (finnat_ind
     (fun (n : nat) (u : FinNat n) =>
      P n (finnat_to_fin u)) (fun n0 : nat => z n0)
     (fun (n' : nat) (u : FinNat n')
        (c : P n' (finnat_to_fin u)) =>
      transport (P n'.+1) (path_finnat_to_fin_succ u)^
        (s n' (finnat_to_fin u) c))
     (fin_to_finnat fin_zero)) = z n
  generalize (path_fin_to_finnat_to_fin (@fin_zero n)).
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
forall
p : finnat_to_fin (fin_to_finnat fin_zero) = fin_zero,
transport (P n.+1) p
  (finnat_ind
     (fun (n : nat) (u : FinNat n) =>
      P n (finnat_to_fin u)) (fun n0 : nat => z n0)
     (fun (n' : nat) (u : FinNat n')
        (c : P n' (finnat_to_fin u)) =>
      transport (P n'.+1) (path_finnat_to_fin_succ u)^
        (s n' (finnat_to_fin u) c))
     (fin_to_finnat fin_zero)) = z n
  induction (path_fin_to_finnat_fin_zero n)^.
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
forall p : finnat_to_fin (zero_finnat n) = fin_zero,
transport (P n.+1) p
  (finnat_ind
     (fun (n : nat) (u : FinNat n) =>
      P n (finnat_to_fin u)) (fun n0 : nat => z n0)
     (fun (n' : nat) (u : FinNat n')
        (c : P n' (finnat_to_fin u)) =>
      transport (P n'.+1) (path_finnat_to_fin_succ u)^
        (s n' (finnat_to_fin u) c)) (zero_finnat n)) =
z n
  intro p.
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
p: finnat_to_fin (zero_finnat n) = fin_zero
transport (P n.+1) p
  (finnat_ind
     (fun (n : nat) (u : FinNat n) =>
      P n (finnat_to_fin u)) (fun n0 : nat => z n0)
     (fun (n' : nat) (u : FinNat n')
        (c : P n' (finnat_to_fin u)) =>
      transport (P n'.+1) (path_finnat_to_fin_succ u)^
        (s n' (finnat_to_fin u) c)) (zero_finnat n)) =
z n
  destruct (hset_path2 1 p).
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
transport (P n.+1) 1
  (finnat_ind
     (fun (n : nat) (u : FinNat n) =>
      P n (finnat_to_fin u)) (fun n0 : nat => z n0)
     (fun (n' : nat) (u : FinNat n')
        (c : P n' (finnat_to_fin u)) =>
      transport (P n'.+1) (path_finnat_to_fin_succ u)^
        (s n' (finnat_to_fin u) c)) (zero_finnat n)) =
z n
  lhs napply transport_1.
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
finnat_ind
  (fun (n : nat) (u : FinNat n) =>
   P n (finnat_to_fin u)) (fun n0 : nat => z n0)
  (fun (n' : nat) (u : FinNat n')
     (c : P n' (finnat_to_fin u)) =>
   transport (P n'.+1) (path_finnat_to_fin_succ u)^
     (s n' (finnat_to_fin u) c)) (zero_finnat n) = 
z n
  napply finnat_ind_beta_zero.
Defined.

Lemma fin_ind_beta_fsucc (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)
  : fin_ind P z s (fsucc k) = s n k (fin_ind P z s k).
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
fin_ind P z s (fsucc k) = s n k (fin_ind P z s k)
Proof.
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
fin_ind P z s (fsucc k) = s n k (fin_ind P z s k)
  unfold fin_ind.
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
transport (P n.+1)
  (path_fin_to_finnat_to_fin (fsucc k))
  (finnat_ind
     (fun (n : nat) (u : FinNat n) =>
      P n (finnat_to_fin u)) (fun n0 : nat => z n0)
     (fun (n' : nat) (u : FinNat n')
        (c : P n' (finnat_to_fin u)) =>
      transport (P n'.+1) (path_finnat_to_fin_succ u)^
        (s n' (finnat_to_fin u) c))
     (fin_to_finnat (fsucc k))) =
s n k
  (transport (P n) (path_fin_to_finnat_to_fin k)
     (finnat_ind
        (fun (n : nat) (u : FinNat n) =>
         P n (finnat_to_fin u)) (fun n0 : nat => z n0)
        (fun (n' : nat) (u : FinNat n')
           (c : P n' (finnat_to_fin u)) =>
         transport (P n'.+1)
           (path_finnat_to_fin_succ u)^
           (s n' (finnat_to_fin u) c))
        (fin_to_finnat k)))
  generalize (path_fin_to_finnat_to_fin (fsucc k)).
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
forall
p : finnat_to_fin (fin_to_finnat (fsucc k)) = fsucc k,
transport (P n.+1) p
  (finnat_ind
     (fun (n : nat) (u : FinNat n) =>
      P n (finnat_to_fin u)) (fun n0 : nat => z n0)
     (fun (n' : nat) (u : FinNat n')
        (c : P n' (finnat_to_fin u)) =>
      transport (P n'.+1) (path_finnat_to_fin_succ u)^
        (s n' (finnat_to_fin u) c))
     (fin_to_finnat (fsucc k))) =
s n k
  (transport (P n) (path_fin_to_finnat_to_fin k)
     (finnat_ind
        (fun (n : nat) (u : FinNat n) =>
         P n (finnat_to_fin u)) (fun n0 : nat => z n0)
        (fun (n' : nat) (u : FinNat n')
           (c : P n' (finnat_to_fin u)) =>
         transport (P n'.+1)
           (path_finnat_to_fin_succ u)^
           (s n' (finnat_to_fin u) c))
        (fin_to_finnat k)))
  induction (path_fin_to_finnat_fsucc k)^.
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
forall
p : finnat_to_fin (succ_finnat (fin_to_finnat k)) =
    fsucc k,
transport (P n.+1) p
  (finnat_ind
     (fun (n : nat) (u : FinNat n) =>
      P n (finnat_to_fin u)) (fun n0 : nat => z n0)
     (fun (n' : nat) (u : FinNat n')
        (c : P n' (finnat_to_fin u)) =>
      transport (P n'.+1) (path_finnat_to_fin_succ u)^
        (s n' (finnat_to_fin u) c))
     (succ_finnat (fin_to_finnat k))) =
s n k
  (transport (P n) (path_fin_to_finnat_to_fin k)
     (finnat_ind
        (fun (n : nat) (u : FinNat n) =>
         P n (finnat_to_fin u)) (fun n0 : nat => z n0)
        (fun (n' : nat) (u : FinNat n')
           (c : P n' (finnat_to_fin u)) =>
         transport (P n'.+1)
           (path_finnat_to_fin_succ u)^
           (s n' (finnat_to_fin u) c))
        (fin_to_finnat k)))
  intro p.
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: finnat_to_fin (succ_finnat (fin_to_finnat k)) =
fsucc k
transport (P n.+1) p
  (finnat_ind
     (fun (n : nat) (u : FinNat n) =>
      P n (finnat_to_fin u)) (fun n0 : nat => z n0)
     (fun (n' : nat) (u : FinNat n')
        (c : P n' (finnat_to_fin u)) =>
      transport (P n'.+1) (path_finnat_to_fin_succ u)^
        (s n' (finnat_to_fin u) c))
     (succ_finnat (fin_to_finnat k))) =
s n k
  (transport (P n) (path_fin_to_finnat_to_fin k)
     (finnat_ind
        (fun (n : nat) (u : FinNat n) =>
         P n (finnat_to_fin u)) (fun n0 : nat => z n0)
        (fun (n' : nat) (u : FinNat n')
           (c : P n' (finnat_to_fin u)) =>
         transport (P n'.+1)
           (path_finnat_to_fin_succ u)^
           (s n' (finnat_to_fin u) c))
        (fin_to_finnat k)))
  refine (ap (transport (P n.+1) p) (finnat_ind_beta_succ _ _ _ _) @ _).
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: finnat_to_fin (succ_finnat (fin_to_finnat k)) =
fsucc k
transport (P n.+1) p
  (transport (P n.+1)
     (path_finnat_to_fin_succ (fin_to_finnat k))^
     (s n (finnat_to_fin (fin_to_finnat k))
        (finnat_ind
           (fun (n : nat) (u : FinNat n) =>
            P n (finnat_to_fin u))
           (fun n0 : nat => z n0)
           (fun (n' : nat) (u : FinNat n')
              (c : P n' (finnat_to_fin u)) =>
            transport (P n'.+1)
              (path_finnat_to_fin_succ u)^
              (s n' (finnat_to_fin u) c))
           (fin_to_finnat k)))) =
s n k
  (transport (P n) (path_fin_to_finnat_to_fin k)
     (finnat_ind
        (fun (n : nat) (u : FinNat n) =>
         P n (finnat_to_fin u)) (fun n0 : nat => z n0)
        (fun (n' : nat) (u : FinNat n')
           (c : P n' (finnat_to_fin u)) =>
         transport (P n'.+1)
           (path_finnat_to_fin_succ u)^
           (s n' (finnat_to_fin u) c))
        (fin_to_finnat k)))
  generalize dependent p.
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
forall
p : finnat_to_fin (succ_finnat (fin_to_finnat k)) =
    fsucc k,
transport (P n.+1) p
  (transport (P n.+1)
     (path_finnat_to_fin_succ (fin_to_finnat k))^
     (s n (finnat_to_fin (fin_to_finnat k))
        (finnat_ind
           (fun (n : nat) (u : FinNat n) =>
            P n (finnat_to_fin u))
           (fun n0 : nat => z n0)
           (fun (n' : nat) (u : FinNat n')
              (c : P n' (finnat_to_fin u)) =>
            transport (P n'.+1)
              (path_finnat_to_fin_succ u)^
              (s n' (finnat_to_fin u) c))
           (fin_to_finnat k)))) =
s n k
  (transport (P n) (path_fin_to_finnat_to_fin k)
     (finnat_ind
        (fun (n : nat) (u : FinNat n) =>
         P n (finnat_to_fin u)) (fun n0 : nat => z n0)
        (fun (n' : nat) (u : FinNat n')
           (c : P n' (finnat_to_fin u)) =>
         transport (P n'.+1)
           (path_finnat_to_fin_succ u)^
           (s n' (finnat_to_fin u) c))
        (fin_to_finnat k)))
  induction (path_fin_to_finnat_to_fin k).
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
forall
p : finnat_to_fin
      (succ_finnat
         (fin_to_finnat
            (finnat_to_fin (fin_to_finnat k)))) =
    fsucc (finnat_to_fin (fin_to_finnat k)),
transport (P n.+1) p
  (transport (P n.+1)
     (path_finnat_to_fin_succ
        (fin_to_finnat
           (finnat_to_fin (fin_to_finnat k))))^
     (s n
        (finnat_to_fin
           (fin_to_finnat
              (finnat_to_fin (fin_to_finnat k))))
        (finnat_ind
           (fun (n : nat) (u : FinNat n) =>
            P n (finnat_to_fin u))
           (fun n0 : nat => z n0)
           (fun (n' : nat) (u : FinNat n')
              (c : P n' (finnat_to_fin u)) =>
            transport (P n'.+1)
              (path_finnat_to_fin_succ u)^
              (s n' (finnat_to_fin u) c))
           (fin_to_finnat
              (finnat_to_fin (fin_to_finnat k)))))) =
s n (finnat_to_fin (fin_to_finnat k))
  (transport (P n) 1
     (finnat_ind
        (fun (n : nat) (u : FinNat n) =>
         P n (finnat_to_fin u)) (fun n0 : nat => z n0)
        (fun (n' : nat) (u : FinNat n')
           (c : P n' (finnat_to_fin u)) =>
         transport (P n'.+1)
           (path_finnat_to_fin_succ u)^
           (s n' (finnat_to_fin u) c))
        (fin_to_finnat k)))
  induction (path_fin_to_finnat_to_fin k)^.
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
forall
p : finnat_to_fin (succ_finnat (fin_to_finnat k)) =
    fsucc (finnat_to_fin (fin_to_finnat k)),
transport (P n.+1) p
  (transport (P n.+1)
     (path_finnat_to_fin_succ (fin_to_finnat k))^
     (s n (finnat_to_fin (fin_to_finnat k))
        (finnat_ind
           (fun (n : nat) (u : FinNat n) =>
            P n (finnat_to_fin u))
           (fun n0 : nat => z n0)
           (fun (n' : nat) (u : FinNat n')
              (c : P n' (finnat_to_fin u)) =>
            transport (P n'.+1)
              (path_finnat_to_fin_succ u)^
              (s n' (finnat_to_fin u) c))
           (fin_to_finnat k)))) =
s n (finnat_to_fin (fin_to_finnat k))
  (transport (P n) 1
     (finnat_ind
        (fun (n : nat) (u : FinNat n) =>
         P n (finnat_to_fin u)) (fun n0 : nat => z n0)
        (fun (n' : nat) (u : FinNat n')
           (c : P n' (finnat_to_fin u)) =>
         transport (P n'.+1)
           (path_finnat_to_fin_succ u)^
           (s n' (finnat_to_fin u) c))
        (fin_to_finnat k)))
  intro p.
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: finnat_to_fin (succ_finnat (fin_to_finnat k)) =
fsucc (finnat_to_fin (fin_to_finnat k))
transport (P n.+1) p
  (transport (P n.+1)
     (path_finnat_to_fin_succ (fin_to_finnat k))^
     (s n (finnat_to_fin (fin_to_finnat k))
        (finnat_ind
           (fun (n : nat) (u : FinNat n) =>
            P n (finnat_to_fin u))
           (fun n0 : nat => z n0)
           (fun (n' : nat) (u : FinNat n')
              (c : P n' (finnat_to_fin u)) =>
            transport (P n'.+1)
              (path_finnat_to_fin_succ u)^
              (s n' (finnat_to_fin u) c))
           (fin_to_finnat k)))) =
s n (finnat_to_fin (fin_to_finnat k))
  (transport (P n) 1
     (finnat_ind
        (fun (n : nat) (u : FinNat n) =>
         P n (finnat_to_fin u)) (fun n0 : nat => z n0)
        (fun (n' : nat) (u : FinNat n')
           (c : P n' (finnat_to_fin u)) =>
         transport (P n'.+1)
           (path_finnat_to_fin_succ u)^
           (s n' (finnat_to_fin u) c))
        (fin_to_finnat k)))
  induction (hset_path2 p (path_finnat_to_fin_succ (fin_to_finnat k))).
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: finnat_to_fin (succ_finnat (fin_to_finnat k)) =
fsucc (finnat_to_fin (fin_to_finnat k))
transport (P n.+1) p
  (transport (P n.+1) p^
     (s n (finnat_to_fin (fin_to_finnat k))
        (finnat_ind
           (fun (n : nat) (u : FinNat n) =>
            P n (finnat_to_fin u))
           (fun n0 : nat => z n0)
           (fun (n' : nat) (u : FinNat n')
              (c : P n' (finnat_to_fin u)) =>
            transport (P n'.+1)
              (path_finnat_to_fin_succ u)^
              (s n' (finnat_to_fin u) c))
           (fin_to_finnat k)))) =
s n (finnat_to_fin (fin_to_finnat k))
  (transport (P n) 1
     (finnat_ind
        (fun (n : nat) (u : FinNat n) =>
         P n (finnat_to_fin u)) (fun n0 : nat => z n0)
        (fun (n' : nat) (u : FinNat n')
           (c : P n' (finnat_to_fin u)) =>
         transport (P n'.+1)
           (path_finnat_to_fin_succ u)^
           (s n' (finnat_to_fin u) c))
        (fin_to_finnat k)))
  apply transport_pV.
Defined.

Definition fin_rec (B : nat -> Type)
  : (forall n : nat, B n.+1) -> (forall (n : nat), Fin n -> B n -> B n.+1) ->
    forall {n : nat}, Fin n -> B n
  := fin_ind (fun n _ => B n).

Lemma fin_rec_beta_zero (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.
B: nat -> Type
z: forall n : nat, B n.+1
s: forall n : nat, Fin n -> B n -> B n.+1
n: nat
fin_rec B z s fin_zero = z n
Proof.
B: nat -> Type
z: forall n : nat, B n.+1
s: forall n : nat, Fin n -> B n -> B n.+1
n: nat
fin_rec B z s fin_zero = z n
  apply (fin_ind_beta_zero (fun n _ => B n)).
Defined.

Lemma fin_rec_beta_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).
B: nat -> Type
z: forall n : nat, B n.+1
s: forall n : nat, 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.
B: nat -> Type
z: forall n : nat, B n.+1
s: forall n : nat, 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)
  apply (fin_ind_beta_fsucc (fun n _ => B n)).
Defined.