theorem :: NTALGO_2:7
Nat2BL . 1 = <*1*>