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; induction Hm as [|[a m] l Hm IHHm Hr]; intros x e H; simpl in *. - inversion H. - apply InA_cons in H; destruct H as [H|H]. * unfold eqke in H; simpl in H. destruct elim_compare_eq with x a as [H' r]; [tauto|]. rewrite r; f_equal; symmetry; tauto. * destruct elim_compare_gt with x a as [H' r]; [|rewrite r; apply IHHm, H]. apply InA_eqke_eqk in H. apply (Sort_Inf_In Hm Hr H). Qed.
imports: FMapInterface