proposition: Lemma compute_fin_ind_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).
proof: Proof. unfold fin_ind. generalize (path_fin_to_finnat_to_fin (fsucc k)). induction (path_fin_to_finnat_fsucc k)^. intro p. refine (ap (transport (P n.+1) p) (compute_finnat_ind_succ _ _ _ _) @ _). generalize dependent p. induction (path_fin_to_finnat_to_fin k). induction (path_fin_to_finnat_to_fin k)^. intro p. induction (hset_path2 p (path_finnat_to_fin_succ (fin_to_finnat k))). apply transport_pV. Defined.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Spaces.Nat.Core HoTT.Spaces.Finite.FinNat HoTT.Spaces.Finite.Fin