proposition: Lemma extensionality : forall A B (IB:Inhab B) (M1 M2:map A B), (forall (k:A), k \indom M1 <-> k \indom M2) -> (forall (k:A), k \indom M1 -> M1[k] = M2[k]) -> M1 = M2.
proof: Proof. Proof using. introv HD HE. extens. intros k. specializes HD k. specializes HE k. unfold dom_inst, dom_impl, read_inst, read_impl in *. simpls. repeat rewrite in_set_st_eq in *. case_eq (M1 k); introv Hv1; rewrite Hv1 in HE,HD; case_eq (M2 k); introv Hv2; try rewrite Hv2 in HE,HD. { forwards* ->: HE. } { false. forwards: (proj1 HD); auto_false. } { false. forwards: (proj2 HD); auto_false. } { auto. } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)