proposition: Lemma gen_tree_of_to_list {T} k l (t : gen_tree T) : gen_tree_of_list k (gen_tree_to_list t ++ l) = gen_tree_of_list (t :: k) l.
proof: Proof. revert t k l; fix FIX 1; intros [|n ts] k l; simpl; auto. trans (gen_tree_of_list (reverse ts ++ k) ([inl (length ts, n)] ++ l)). - rewrite <-(assoc_L _). revert k. generalize ([inl (length ts, n)] ++ l). induction ts as [|t ts'' IH]; intros k ts'''; csimpl; auto. rewrite reverse_cons, <-!(assoc_L _), FIX; simpl; auto. - simpl. by rewrite take_app_length', drop_app_length', reverse_involutive by (by rewrite reverse_length). Qed.
imports: Coq.QArith(QArith_base Qcanon) stdpp(well_founded) stdpp(options)