proposition: Lemma vec_card `{Finite A} n : card (vec A n) = card A ^ n.
proof: Proof. unfold card; simpl. induction n as [|n IH]; simpl; [done|]. rewrite <-IH. clear IH. generalize (vec_enum (enum A) n). induction (enum A) as [|x xs IH]; intros l; csimpl; auto. by rewrite app_length, fmap_length, IH. Qed.
imports: stdpp(options)