proposition: Theorem flatten_valid_A_2 : forall (t t':bin)(l:list A)(def:A), bin_A l def (flatten t) = bin_A l def (flatten t')-> bin_A l def t = bin_A l def t'.
proof: Proof. intros t t' l def Heq. rewrite (flatten_valid_A l def t); now rewrite (flatten_valid_A l def t'). Qed.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure Zdiv