proposition: Lemma find_1 : forall m (Hm:Sort m) x e, MapsTo x e m -> find x m = Some e.
proof: Proof. intros m Hm x e; generalize Hm; clear Hm; unfold MapsTo. induction m as [ |[k' _x] l IHb];simpl; subst; try clear H_eq_1. - inversion 2. - case_eq (compare x k'); intros _x0 e1; subst. + inversion_clear 2. * clear e1;compute in H0; destruct H0. apply lt_not_eq in H; auto with smtcoq_array. now contradict H. * clear e1;generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute. intros. apply (lt_trans k') in _x0; auto with smtcoq_array. apply lt_not_eq in _x0. now contradict _x0. + clear e1;inversion_clear 2. * compute in H0; destruct H0; intuition congruence. * generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute. intros. apply lt_not_eq in H. now contradict H. + clear e1; do 2 inversion_clear 1; auto with smtcoq_array. compute in H2; destruct H2. subst. apply lt_not_eq in _x0. now contradict _x0. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance