proposition: Lemma elements_equation (r : t) : elements r = elements_def r.
proof: Proof. funelim (elements r); simp elements_def; trivial. f_equal. induction l; simpl; auto. simp map_In. rewrite H. rewrite IHl; auto. intros. apply H. now constructor 2. now constructor. Qed.
imports: Program Equations(Equations) Utf8 Lia Arith List