Let X be given.
Assume Hunc: uncountable_set X.
Assume Heq: X = Empty.
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim HcountE: countable_set Empty.
We will prove countable_set Empty.
We will prove countable Empty.
An exact proof term for the current goal is countable_Empty.
We prove the intermediate claim HcountX: countable_set X.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HcountE.
An exact proof term for the current goal is (Hunc HcountX).
∎