proposition: Lemma extensionality_of_dom_eq : forall A B (IB:Inhab B) (M1 M2:map A B), (dom M1 = dom M2) -> (forall (k:A), k \indom M1 -> M1[k] = M2[k]) -> M1 = M2.
proof: Proof. Proof using. introv E Hk. applys extensionality. { rewrite* E. } { applys Hk. } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)