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