proposition: Lemma pickle_taggedK : pcancel pickle_tagged unpickle_tagged.
proof: Proof. by case=> i x; rewrite /unpickle_tagged CodeSeq.codeK /= pickleK /= pickleK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)