proposition: Lemma restrict_in_iff : forall m m' k, In k (restrict m m') <-> In k m /\ In k m'.
proof: Proof. intros m m' k. split. - intros (e,H); rewrite restrict_mapsto_iff in H. destruct H; split; auto. exists e; auto. - intros ((e,H),H'); exists e; rewrite restrict_mapsto_iff; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface