Haskellで下記のデータ型を定義した時にBinat -> Nat型の単射な関数が思いつかず、タイトルの仮説が浮かんだ次第。
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]$の各実数を二進数の無限小数で一意1に表したものと一対一に対応するので、$B_2 \setminus B_1$の濃度は連続体濃度。
以上より、Binat型のすべての値の集合は連続体濃度2。