proposition: Lemma compress_equiv `{EqDec k} m : m ≈ compress m.
proof: Proof. apply FunctionalElimination_compress; repeat intro; auto. simpl in *. rewrite <- X. rewrite lookup_delete. now destruct (eq_dec k0 i'). Qed.
imports: Coq.Lists.List Coq.micromega.Lia Equations(Equations) Category.Lib