HoTT.Spaces.Finite.FinInduction.v.alectryon.json

Require ImportRequire Import
  HoTT.Basics
  HoTT.Types
  HoTT.Universes.HSet
  HoTT.Spaces.Nat.Core
  HoTT.Spaces.Finite.FinNat
  HoTT.Spaces.Finite.Fin.

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 n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k0 : Fin n0), P n0 k0 -> P n0.+1 (fsucc k0)
n: nat
k: Fin n
P n k
Proof.P: forall n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k0 : Fin n0), P n0 k0 -> P n0.+1 (fsucc k0)
n: nat
k: Fin n
P n k
  refine (transport (P n) (path_fin_to_finnat_to_fin k) _).P: forall n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k0 : Fin n0), P n0 k0 -> P n0.+1 (fsucc k0)
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 n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k0 : Fin n0), P n0 k0 -> P n0.+1 (fsucc k0)
n: nat
k: Fin n
forall n0 : nat, P n0.+1 (finnat_to_fin (zero_finnat n0))
P: forall n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k0 : Fin n0), P n0 k0 -> P n0.+1 (fsucc k0)
n: nat
k: Fin n
forall (n0 : nat) (u : FinNat n0),
P n0 (finnat_to_fin u) -> P n0.+1 (finnat_to_fin (succ_finnat u))
  -P: forall n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k0 : Fin n0), P n0 k0 -> P n0.+1 (fsucc k0)
n: nat
k: Fin n
forall n0 : nat, P n0.+1 (finnat_to_fin (zero_finnat n0)) intro.P: forall n1 : nat, Fin n1 -> Type
z: forall n1 : nat, P n1.+1 fin_zero
s: forall (n1 : nat) (k0 : Fin n1), P n1 k0 -> P n1.+1 (fsucc k0)
n: nat
k: Fin n
n0: nat
P n0.+1 (finnat_to_fin (zero_finnat n0)) apply z.
  -P: forall n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k0 : Fin n0), P n0 k0 -> P n0.+1 (fsucc k0)
n: nat
k: Fin n
forall (n0 : nat) (u : FinNat n0),
P n0 (finnat_to_fin u) -> P n0.+1 (finnat_to_fin (succ_finnat u)) intros n' u c.P: forall n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k0 : Fin n0), P n0 k0 -> P n0.+1 (fsucc k0)
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 n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k0 : Fin n0), P n0 k0 -> P n0.+1 (fsucc k0)
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 n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k : Fin n0), P n0 k -> P n0.+1 (fsucc k)
n: nat
fin_ind P z s fin_zero = z n
Proof.P: forall n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k : Fin n0), P n0 k -> P n0.+1 (fsucc k)
n: nat
fin_ind P z s fin_zero = z n
  unfold fin_ind.P: forall n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k : Fin n0), P n0 k -> P n0.+1 (fsucc k)
n: nat
transport (P n.+1) (path_fin_to_finnat_to_fin fin_zero)
  (finnat_ind (fun (n0 : nat) (u : FinNat n0) => P n0 (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 n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k : Fin n0), P n0 k -> P n0.+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 (n0 : nat) (u : FinNat n0) => P n0 (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 n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k : Fin n0), P n0 k -> P n0.+1 (fsucc k)
n: nat
forall p : finnat_to_fin (zero_finnat n) = fin_zero,
transport (P n.+1) p
  (finnat_ind (fun (n0 : nat) (u : FinNat n0) => P n0 (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 n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k : Fin n0), P n0 k -> P n0.+1 (fsucc k)
n: nat
p: finnat_to_fin (zero_finnat n) = fin_zero
transport (P n.+1) p
  (finnat_ind (fun (n0 : nat) (u : FinNat n0) => P n0 (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 n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k : Fin n0), P n0 k -> P n0.+1 (fsucc k)
n: nat
transport (P n.+1) 1
  (finnat_ind (fun (n0 : nat) (u : FinNat n0) => P n0 (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 n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k : Fin n0), P n0 k -> P n0.+1 (fsucc k)
n: nat
finnat_ind (fun (n0 : nat) (u : FinNat n0) => P n0 (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 n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k0 : Fin n0), P n0 k0 -> P n0.+1 (fsucc k0)
n: nat
k: Fin n
fin_ind P z s (fsucc k) = s n k (fin_ind P z s k)
Proof.P: forall n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k0 : Fin n0), P n0 k0 -> P n0.+1 (fsucc k0)
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 n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k0 : Fin n0), P n0 k0 -> P n0.+1 (fsucc k0)
n: nat
k: Fin n
transport (P n.+1) (path_fin_to_finnat_to_fin (fsucc k))
  (finnat_ind (fun (n0 : nat) (u : FinNat n0) => P n0 (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 (n0 : nat) (u : FinNat n0) => P n0 (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 n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k0 : Fin n0), P n0 k0 -> P n0.+1 (fsucc k0)
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 (n0 : nat) (u : FinNat n0) => P n0 (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 (n0 : nat) (u : FinNat n0) => P n0 (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 n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k0 : Fin n0), P n0 k0 -> P n0.+1 (fsucc k0)
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 (n0 : nat) (u : FinNat n0) => P n0 (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 (n0 : nat) (u : FinNat n0) => P n0 (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 n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k0 : Fin n0), P n0 k0 -> P n0.+1 (fsucc k0)
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 (n0 : nat) (u : FinNat n0) => P n0 (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 (n0 : nat) (u : FinNat n0) => P n0 (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 n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k0 : Fin n0), P n0 k0 -> P n0.+1 (fsucc k0)
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 (n0 : nat) (u : FinNat n0) => P n0 (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 (n0 : nat) (u : FinNat n0) => P n0 (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 n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k0 : Fin n0), P n0 k0 -> P n0.+1 (fsucc k0)
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 (n0 : nat) (u : FinNat n0) => P n0 (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 (n0 : nat) (u : FinNat n0) => P n0 (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 n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k0 : Fin n0), P n0 k0 -> P n0.+1 (fsucc k0)
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 (n0 : nat) (u : FinNat n0) => P n0 (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 (n0 : nat) (u : FinNat n0) => P n0 (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 n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k0 : Fin n0), P n0 k0 -> P n0.+1 (fsucc k0)
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 (n0 : nat) (u : FinNat n0) => P n0 (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 (n0 : nat) (u : FinNat n0) => P n0 (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 n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k0 : Fin n0), P n0 k0 -> P n0.+1 (fsucc k0)
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 (n0 : nat) (u : FinNat n0) => P n0 (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 (n0 : nat) (u : FinNat n0) => P n0 (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 n0 : nat, Fin n0 -> Type
z: forall n0 : nat, P n0.+1 fin_zero
s: forall (n0 : nat) (k0 : Fin n0), P n0 k0 -> P n0.+1 (fsucc k0)
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 (n0 : nat) (u : FinNat n0) => P n0 (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 (n0 : nat) (u : FinNat n0) => P n0 (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 n0 : nat, B n0.+1
s: forall n0 : nat, Fin n0 -> B n0 -> B n0.+1
n: nat
fin_rec B z s fin_zero = z n
Proof.B: nat -> Type
z: forall n0 : nat, B n0.+1
s: forall n0 : nat, Fin n0 -> B n0 -> B n0.+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 n0 : nat, B n0.+1
s: forall n0 : nat, Fin n0 -> B n0 -> B n0.+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 n0 : nat, B n0.+1
s: forall n0 : nat, Fin n0 -> B n0 -> B n0.+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.