Direct conversion of framed Boolean lists to raw words

The canonical ComputableInPolyTime.listToBits certificate keeps its original public contract and registration. Its proof reuses the linear streaming conversion certificate, without a fold over a growing 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.