fact: Fixpoint tree_encode (t : bintree) : GenTree.tree unit := match t with | BinLeaf => GenTree.Leaf tt | BinNode tl tr => GenTree.Node 2 [:: tree_encode tl; tree_encode tr] end.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype