baz_num_elts exercise from Software Foundations
I agree with you. There's a bijection between baz and False.

Definition injective : forall {t1 t2}, (t1 -&gt; t2) -&gt; Prop := fun t1 t2 f1 =&gt; forall x1 x2, f1 x1 = f1 x2 -&gt; x1 = x2.

Definition surjective : forall {t1 t2}, (t1 -&gt; t2) -&gt; Prop := fun t1 t2 f1 =&gt; forall x1, exists x2, f1 x2 = x1.

Definition bijective : forall {t1 t2}, (t1 -&gt; t2) -&gt; Prop := fun t1 t2 f1 =&gt; injective f1 /\ surjective f1.

Inductive baz : Type :=
   | x : baz -&gt; baz
   | y : baz -&gt; bool -&gt; baz.

Theorem baz_False : baz -&gt; False. Proof. induction 1; firstorder. Qed.

Goal exists f1 : baz -&gt; False, bijective f1.
Proof.
exists baz_False. unfold bijective, injective, surjective. firstorder.
assert (H2 := baz_False x1). firstorder.
assert (H2 := x1). firstorder.
Qed.