fact: Definition same_sum_leaves (l1 l2 : list (btree A)) : Prop := exists l3 : list (btree A), (exists l4 : list (btree A), Permutation l1 l3 /\ Permutation l2 l4 /\ map (sum_leaves f) l3 = map (sum_leaves f) l4).
imports: Coq(Sorting.Permutation)