`{Funext} X `{Finite X} n : finmult (fun x:X => n) = nat_pow n (fcard X). Proof. refine (fcard_arrow X (Fin n)). Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import Spaces.Nat.Core Spaces.Nat.Factorial. Require Import HFiber. Require Import Factorization. Require Import Truncations. Require Import Colimits.Quotient. Require Import Projective. Require Import Fin.