proposition: Theorem flatten_aux_valid_A: forall (l : list A) (t t' : bin), f (bin_A l t) (bin_A l t') = bin_A l (flatten_aux t t').
proof: Proof. intros l t; elim t; simpl; auto. intros t1 IHt1 t2 IHt2 t'; rewrite <- IHt1; rewrite <- IHt2. symmetry; apply assoc. Qed.
imports: ZArith List Arith Zwf Relations Inverse_Image Transitive_Closure Zdiv