4 ms·
Yep, and you could even prove "nat" is isomorphic to the type of binary numbers "Bin := List (0 | 1)" and transport proofs there too.
by pgustafs 6y ago
Yep, and you could even prove "nat" is isomorphic to the type of binary numbers "Bin := List (0 | 1)" and transport proofs there too.