proposition: Lemma elements2_equation r acc : elements_acc r acc = elements_def r ++ acc.
proof: Proof. revert r acc. let t := constr:(fun_elim (f:=elements_acc)) in apply (t (fun r acc res => res = elements_def r ++ acc) (fun r acc x H res => res = concat (List.map elements_def x) ++ acc)); intros; simp elements; trivial. rewrite H1. clear H1. rewrite H0. simpl. now rewrite app_assoc. Qed.
imports: Program Equations(Equations) Utf8 Lia Arith List