fact: Definition m_btree (A:Set) (bt:btree A) := match bt with Empty => nil | (Node bt1 x bt2) => (cons (btree_size A bt) (cons (btree_size A bt1) nil)) end.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef