proposition: Theorem gsident {A} i (m:t A) v : find i m = Some v -> add i v m = m.
proof: Proof. revert m. induction i; destruct m; simpl in *; try congruence. - intro H; now rewrite (IHi m2 H). - intro H; now rewrite (IHi m1 H). Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)