proposition: Theorem one_step_weight_tree_list : forall l1 l2 l3 : list (btree A), one_step l1 l2 -> one_step l1 l3 -> weight_tree_list f l2 = weight_tree_list f l3.
proof: Proof. intros l1 l2 l3 (l4, (t1, (t2, (H1, (H2, H3))))) (l5, (t3, (t4, (H4, (H5, H6))))). rewrite weight_tree_list_permutation with (1 := H3). rewrite weight_tree_list_permutation with (1 := H6). repeat rewrite weight_tree_list_node. apply f_equal2 with (f := plus). cut (map (sum_leaves f) (t1 :: t2 :: l4) = map (sum_leaves f) (t3 :: t4 :: l5)). simpl in |- *; intros H7; injection H7. intros H8 H9 H10; repeat apply f_equal2 with (f := plus); auto. apply ordered_sum_leaves_eq; auto. apply Permutation_trans with (2 := H5); auto. apply Permutation_sym; auto. rewrite <- weight_tree_list_permutation with (1 := H2). apply weight_tree_list_permutation; auto. Qed.
imports: Coq(Sorting.Permutation)