fact: Definition decode_step c fs := match c with | inr x => (Leaf x :: fs.1, fs.2) | inl 0 => ([::], fs.1 :: fs.2) | inl n.+1 => (Node n fs.1 :: head [::] fs.2, behead fs.2) end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)