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