proposition: Theorem one_step_same_sum_leaves : forall l1 l2 l3 : list (btree A), one_step l1 l2 -> one_step l1 l3 -> same_sum_leaves f l2 l3.
proof: Proof. intros l1 l2 l3 (l4, (t1, (t2, (H1, (H2, H3))))) (l5, (t3, (t4, (H4, (H5, H6))))). Proof. red in |- *. exists (node t1 t2 :: l4); exists (node t3 t4 :: l5); auto; simpl in |- *; auto. split; auto; split; auto. 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; apply f_equal2 with (f := cons (A:=nat)); auto. apply ordered_sum_leaves_eq; auto. apply Permutation_trans with (2 := H5); auto. apply Permutation_sym; auto. Qed.
imports: Coq(Sorting.Permutation)