proposition: Lemma elements'_equation (r : t) : elements' r = elements'_def r.
proof: Proof. pose (fun_elim (f:=elements')). apply (p (fun r f => f = elements'_def r) (fun l x H r => r = concat (List.map elements' x))); clear p; intros; simp elements'_def; trivial. simpl. f_equal. apply H1. Qed.
imports: Program Equations(Equations) Utf8 Lia Arith List