proposition: Lemma MapsTo_inj : forall x e e' l (Hl:Sort l), MapsTo x e l -> MapsTo x e' l -> e = e'.
proof: Proof. induction l. - intros. apply empty_1 in H. contradiction. - intros. destruct a as (y, v). pose proof H as HH. pose proof H0 as HH0. unfold MapsTo in H. apply InA_eqke_eqk in H. apply InA_eqke_eqk in H0. apply (Sort_In_cons_2 Hl) in H. apply (Sort_In_cons_2 Hl) in H0. destruct H, H0. + apply ltk_not_eqk in H. apply ltk_not_eqk in H0. assert (~ eqk (x, e) (y, v)). unfold not in *. intros. apply H. now apply eqk_sym. assert (~ eqk (x, e') (y, v)). unfold not in *. intros. apply H. now apply eqk_sym. specialize (In_inv_3 HH0 H2). specialize (In_inv_3 HH H1). inversion_clear Hl. apply (IHl H3). + apply ltk_not_eqk in H. unfold eqk in H, H0; simpl in H, H0. contradiction. + apply ltk_not_eqk in H0. unfold eqk in H, H0; simpl in H, H0. contradiction. + unfold eqk in H, H0. simpl in *. subst. inversion_clear HH. inversion_clear HH0. unfold eqke in *. simpl in *. destruct H, H1; subst; auto. apply InA_eqke_eqk in H1. inversion_clear Hl. specialize (Sort_Inf_In H2 H3 H1). unfold ltk. simpl. intro. apply lt_not_eq in H4. contradiction. apply InA_eqke_eqk in H. inversion_clear Hl. specialize (Sort_Inf_In H1 H2 H). unfold ltk. simpl. intro. apply lt_not_eq in H3. contradiction. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance