proposition: Lemma compute_fin_ind_fin_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.
proof: Proof. unfold fin_ind. generalize (path_fin_to_finnat_to_fin (@fin_zero n)). induction (path_fin_to_finnat_fin_zero n)^. intro p. destruct (hset_path2 1 p). cbn. by destruct (hset_path2 1 (path_zero_finnat n leq_1_Sn)). Defined.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Spaces.Nat.Core HoTT.Spaces.Finite.FinNat HoTT.Spaces.Finite.Fin