proposition: Lemma elements_correct (r : rose) acc : elements r acc = elements_spec r ++ acc.
proof: Proof. apply (elements_elim (fun r acc f => f = elements_spec r ++ acc) (fun l acc x H r => r = concat (List.map elements_spec x) ++ acc)); intros; simp elements_spec; simpl; trivial. now rewrite H1, H0, app_assoc. Qed.
imports: Equations(Equations) Lia Utf8 List List