The initial assumption about such types having at most countably many elements is false. We can use inductive types to define a non-countable type, namely the countably branching trees:
(* Countably branching trees. *)
Inductive Tree : Type :=
| Leaf : Tree
| Node : (nat -> Tree) -> Tree.
Lemma nocycle (t : Tree) : forall (f : nat -> Tree), t = ...