for n being non zero Nat
for l, m being Nat st l,m are_congruent_mod 2 to_power n holds
n -BinarySequence l = n -BinarySequence m