Haskellで下記のデータ型を定義した時にBinat -> Nat型の単射な関数が思いつかず、タイトルの仮説が浮かんだ次第。

.hs

data Nat = Zero | Succ Nat

data Binat = Bizero | LSucc Binat | RSucc Binat

なんでそう思ったかの概略

証明する気はないが、なんで実数（とBinat型のすべての値の集合の濃度が同じ）と思ったか、概略を述べておく。

まず、LSuccとRSuccをBizeroに有限回適用して得られる値の集合$B_0$は可算無限集合。
次に、RSuccは有限回、LSuccは可算無限回Bizeroに適用して得られる値の集合$B_1$も可算無限集合。
最後に、LSuccとRSuccをBizeroに可算無限回適用して得られる値の集合を$B_2$として、差集合$B_2 \setminus B_1$を考える。LSuccを0、RSuccを1と読み替えれば、半開区間$(0, 1]$の各実数を二進数の無限小数で一意¹に表したものと一対一に対応するので、$B_2 \setminus B_1$の濃度は連続体濃度。
以上より、Binat型のすべての値の集合は連続体濃度²。

0.1とか0.1000...は0.0111...の表記に統一すると一意になる。なお、0.1の有限小数の表記は$B_0$に、0.1000...のゼロが無限に続く表記は$B_1$にそれぞれ対応するイメージ ↩
正確にはx = LSucc xみたいなBizeroを含まない奴らも考えてあげないといけないが、リストのreverseのような関数を想定すれば$B_2$の値と一対一対応するので無視して良いかなって感じがある ↩