proposition: Theorem remove_incl : forall A x dom (m : t A dom), incl (remove x m) m.
proof: Proof. intros * x v Hin. rewrite remove_Some in Hin. intuition. Qed.
imports: Utf8 Bool SetoidList RelationPairs Orders Coqlib DepMapInterface DepMapFactsInterface