[Agda] proofs for binary conversion

[Sergei Meshveliani]

I wrote earlier about    

  an Agda proof for  suc - isomorphism between  ℕ  and its binary codes

on    http://botik.ru/pub/local/Mechveliani/agdaNotes/bin2.zip 

Now, for the occasion that anybody looked there:
I have updated it with a bit simplified version.

The drawback was that I used the  ...List.Pointwise  equality on  Bin⁺
and the construct
                   b=b' ∷p bs=bs

to build an equality proof for bit lists. This was awkward, because the
Bit equality is syntactical. But I somehow failed to use  _≡_ for Bin⁺,
and suffered of complication.

Finally, I recall of the possibility of  PropEq.cong₂ _∷_. 
Now, this enables to plainly use 
                             _≡_   and  PropEq.cong₂ _∷_ b=b' bs=bs'.

Regards,

------
Sergei