proposition: Lemma extend_in_iff : forall m m' k, In k (extend m m') <-> In k m \/ In k m'.
proof: Proof. intros m m' k. split. intros (e,H); rewrite extend_mapsto_iff in H. destruct H; [right|left]; exists e; intuition. destruct (In_dec m' k) as [H|H]. destruct H as (e,H). intros _; exists e. rewrite extend_mapsto_iff; left; auto. destruct 1 as [H'|H']; [|elim H; auto]. destruct H' as (e,H'). exists e. rewrite extend_mapsto_iff; right; auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)