proposition: Lemma in_bindings_uniq k k' v v' (m:t elt) `{!Ok m}: List.In (k,v) (bindings m) -> List.In (k',v') (bindings m) -> k == k' -> k = k' /\ v = v'.
proof: Proof. induction m as [|c l IHl x e r IHr]. - now cbn. - rewrite !bindings_node, !in_app_iff. simpl. invok. intros [INl|[[= <- <-]|INl]] [INr|[[= <- <-]|INr]] E; eauto; try apply in_bindings in INl; try apply in_bindings in INr; order. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)