fact: Fixpoint encode t : seq (nat + T) := match t with | Leaf x => [:: inr _ x] | Node n f => inl _ n.+1 :: rcons (flatten (map encode f)) (inl _ 0) end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)