fact: Fixpoint list_btree_size (A:Set) (bts:list (btree A)) : nat := match bts with nil => 0 | (cons bt bts) => (plus (btree_size A bt) (list_btree_size A bts)) end.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef