proposition: Theorem build_same_weight_tree : forall (l : list (btree A)) (t1 t2 : btree A), build l t1 -> build l t2 -> weight_tree f t1 = weight_tree f t2.
proof: Proof. intros l t1 t2 H H0; apply build_comp with (l1 := l) (l2 := l); auto. exists l; exists l; simpl in |- *; auto. Qed.
imports: Coq(ArithRing Sorting.Permutation)