proposition: Lemma compress_delete `{EqDec k} i m : compress (delete i m) = delete i (compress m).
proof: Proof. generalize dependent i. apply FunctionalElimination_compress; simpl; intros; auto. destruct (eq_dec i i') eqn:Heqe. - subst. rewrite <- H1. now rewrite delete_idem. - simp compress; simpl. f_equal. rewrite <- H1. now rewrite delete_comm. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Equations(Equations) Category.Lib