Is a system of equations derived from mutually recursive ADTs always uniquely solvable?
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 -&gt; Tree) -&gt; Tree.

Lemma nocycle (t : Tree) : forall (f : nat -&gt; Tree), t = Node f -&gt; forall a, f a &lt;&gt; t.
Proof.
  induction t as [? | f H].
  - easy.
  - intros g E n.
    injection E.
    intro E'; destruct E'.
    intro gN.
    now elim (H n f gN n).
Qed.

Corollary uncountable_Tree :
  ~ exists (f : nat -&gt; Tree), forall t : Tree, exists n, f n = t.
Proof.
  intros [f H].
  destruct (H (Node f)) as [n ?].
  now pose (nocycle (Node f) f eq_refl n).
Qed.

In any case, counting elements of types is a tricky business. Consider the following inductive type:
Inductive cow (P : Prop) : Type :=
  | moo : P -&gt; cow P.

Consider any propostion Q : Prop. If cow Q has zero elements then Q is false, and if it has an element then Q is true. So if we could count the elements of cow, we could also tell whether it has zero elements, and would be able to decide an arbitrary proposition, which would give us excluded middle.
You need to restrict the inductive types quite severaly to obtain a small enough family of them whose sizes can actually be counted.