Remove ridiculous automatic rewrite from churchDBTheory

(I put it in there in the first place, of course.)

Fix some knock-on breakages. Also start to formulate converse of
Kraft inequality.

Tidy up a number of things, moving common bl stuff to boolLists

Fix pfreefnsTheory to actually build

More useful facts about universal prefix free machine

Establish λ-term Upf that is a universal machine for pfree fns

In particular, Upf @@ church (M ⊗ x) is the result of machine M on x
if M is prefix-free. If M is not, then the behaviour is of a
prefix-free subset of M's domain.

Start on showing existence of computable prefix-free U machine