I like this Kata, but like so many other functional language katas it's probably assuming too much familiarity with the problem that needs to be solved.
For users too unfamiliar with those concepts, it's too hard to solve them, for those who know them, it seems trivial.

In this kata, apparently Haskell type and function notation is used to "explain" how to tackle the problem in LC, which assumes Haskell knowledge, for instance the difference between types and constructors.

Similarly, the sentence "This means that Scott encoded instances can be deconstructed, simply by providing a case for each option." requires quite a lot of reading and rereading, and assumes parallels to Haskell.

And in a typical Haskellian attitude, authors often ignore semantics in their description, even claim that types signatures are a sufficient substitute for semantics.
They tend to ignore that they're putting pseudo-semantic information into the NAMES of functions, and these names refer to concepts the authors (!) are familiar with.

In this kata, one example of this, is in the definition of Zero and Succ, and pred.

Please reread the description and try to see where you made such assumptions and try to clarify.
Else mark it as a puzzle, but as the kata is labeled 6 Kyu, I think it's better to add clarification.

(typo: corrospond -> correspond)

(you can remove the issue after you've considered my remarks)

( LC )

Check return values for illegally zero-padded BinaryScott numbers. ( I could help out with code for that ).