proposition: Lemma bindings_remove: forall {elt} k tab k' y, InA (keyb_eq (elt:=elt)) (k',y) (bindings (remove k tab)) <-> InA (keyb_eq (elt:=elt)) (k',y) (List.filter (fun p => negb (eqb (fst p) k)) (bindings tab)).
proof: Proof. intros. rewrite filter_InA. 2:{ intros ? ? [? _]; simpl in *; f_equal. unfold key in *. destruct (eqb (fst x) k) eqn:?H, (eqb (fst y0) k) eqn:?H; auto. apply eqb_eq in H0; rewrite H in H0; apply eqb_eq in H0; congruence. apply eqb_eq in H1; rewrite <- H in H1; apply eqb_eq in H1; congruence. } rewrite <- !bindings_mapsto_iff. rewrite remove_mapsto_iff. simpl. split; intros [? ?]; split; auto. destruct (eqb k' k) eqn:?H; auto. apply eqb_eq in H1. symmetry in H1; contradiction. intro. symmetry in H1. apply eqb_eq in H1. rewrite H1 in H0; discriminate. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)