Prove isomorphism

We have tests and we have reasonable confidence in those tests, nonetheless it would be interesting to introduce a proof that `decode . encode = identity`. Maybe something like that would work: 

```idris
proofIso : (str : String) -> {auto prf : IsMultiBase str} -> decode (encode str) = Right str
```