proposition: Lemma map_not_Forall2 (m1 : M A) (m2 : M B) : ¬map_relation R P Q m1 m2 ↔ ∃ i, (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ ¬R x y) ∨ (∃ x, m1 !! i = Some x ∧ m2 !! i = None ∧ ¬P x) ∨ (∃ y, m1 !! i = None ∧ m2 !! i = Some y ∧ ¬Q y).
proof: Proof. split. - rewrite map_relation_alt, (map_not_Forall _). intros (i&?&Hm&?); exists i. rewrite lookup_merge in Hm. destruct (m1 !! i), (m2 !! i); naive_solver auto 2 using bool_decide_pack. - unfold map_relation, option_relation. by intros [i[(x&y&?&?&?)|[(x&?&?&?)|(y&?&?&?)]]] Hm; specialize (Hm i); simplify_option_eq. Qed.
imports: Coq(Permutation) stdpp(options)