proposition: Lemma submap_1 : forall m (Hm:NoDupA m) m' (Hm': NoDupA 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. + destruct H3 as (e', H3). unfold check at 2; rewrite (find_1 Hm' H3). rewrite (H0 t0); simpl; auto. eapply IHm; auto. split; intuition. * apply H. destruct H5 as (e'',H5); exists e''; auto. * apply H0 with k; auto. Qed.
imports: FMapInterface