proposition: Lemma submap_1 : forall m (Hm:Ok m) m' (Hm': Ok m') cmp, Submap cmp m m' -> submap cmp m m' = true.
proof: Proof. unfold Submap, submap. induction m. simpl; auto. destruct a; simpl; intros. destruct H. inversion_clear Hm. assert (H3 : In t0 m'). { apply H; exists e; auto with *. } destruct H3 as (e', H3). assert (H4 : find t0 m' = Some e') by now apply find_spec. unfold check at 2. rewrite H4. rewrite (H0 t0); simpl; auto with *. eapply IHm; auto. split; intuition. apply H. destruct H6 as (e'',H6); exists e''; auto. apply H0 with k; auto. Qed.
imports: Coq(EqualitiesFacts)