proposition: Theorem same_sum_leaves_length : forall l1 l2 : list (btree A), same_sum_leaves l1 l2 -> length l1 = length l2.
proof: Proof. intros l1 l2 (l3, (l4, (H0, (H1, H2)))). rewrite (Permutation_length H0). rewrite (Permutation_length H1). repeat rewrite <- (map_length (sum_leaves f)); auto. apply f_equal with (f := length (A:=nat)); auto. Qed.
imports: Coq(Sorting.Permutation)