proposition: Lemma list_elements_spec {A} (l : list (tree A)) : list_elements l = List.concat (List.map elements l).
proof: Proof. induction l; simp elements; trivial. rewrite IHl. simpl. auto. Qed.
imports: Equations(Equations) Coq.Lists.List