proposition: Lemma toList_fromList (l : list (k * v)) : toList (fromList l) = l.
proof: Proof. induction l; simpl; auto. destruct a; simpl. now rewrite IHl. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Equations(Equations) Category.Lib