theorem :: NTALGO_2:9
Nat2BL . 2 = <*0,1*>