proposition: Lemma submap_2 : forall m (Hm:NoDupA m) m' (Hm': NoDupA m') cmp, submap cmp m m' = true -> Submap cmp m m'.
proof: Proof. unfold Submap, submap. induction m. - simpl; auto. intuition. + destruct H0; inversion H0. + inversion H0. - destruct a; simpl; intros. inversion_clear Hm. rewrite andb_b_true in H. assert (check cmp t0 e m' = true). + clear H1 H0 Hm' IHm. set (b:=check cmp t0 e m') in *. generalize H; clear H; generalize b; clear b. induction m; simpl; auto; intros. destruct a; simpl in *. destruct (andb_prop _ _ (IHm _ H)); auto. + rewrite H2 in H. destruct (IHm H1 m' Hm' cmp H); auto. unfold check in H2. case_eq (find t0 m'); [intros e' H5 | intros H5]; rewrite H5 in H2; try discriminate. split; intros. * destruct H6 as (e0,H6); inversion_clear H6. -- compute in H7; destruct H7; subst. exists e'. apply PX.MapsTo_eq with t0; auto. apply find_2; auto. -- apply H3. exists e0; auto. * inversion_clear H6. -- compute in H8; destruct H8; subst. rewrite (find_1 Hm' (PX.MapsTo_eq H6 H7)) in H5; congruence. -- apply H4 with k; auto. Qed.
imports: FMapInterface