Direct conversion of framed Boolean lists to raw words

The canonical ComputableInPolyTime.listToBits certificate keeps its original public contract and registration. Its direct proof prepends into a raw word with a reachable-prefix bound and then reverses that word. The higher bit-string facade reexports this same declaration.

theorem Turing.MultiTapeTM.ComputableInPolyTime.listToBits : ComputableInPolyTime (fun (l : List Bool) => l) (encList encBool) encBits

Convert framed Boolean lists to raw words without changing their contents.