proposition: Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.
proof: Proof. intros m x. unfold MapsTo. induction m as [ |[k' _x] l IHb];simpl; intro e';try now (intro eqfind; inversion eqfind; auto with smtcoq_array). case_eq (compare x k'); intros _x0 e0 eqfind; inversion eqfind; auto with smtcoq_array. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance