theorem :: NTALGO_2:10
Nat2BL . 3 = <*1,1*>