proposition: Lemma codeK : pcancel encode decode.
proof: Proof. move=> t; rewrite /decode; set fs := (_, _). suffices ->: foldr decode_step fs (encode t) = (t :: fs.1, fs.2) by []. elim: t => //= n f IHt in (fs) *; elim: f IHt => //= t f IHf []. by rewrite rcons_cat foldr_cat => -> /= /IHf[-> -> ->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)