proposition: Lemma map_relation_alt (m1 : M A) (m2 : M B) : map_relation R P Q m1 m2 ↔ map_Forall (λ _, Is_true) (merge f m1 m2).
proof: Proof. split. - intros Hm i P'; rewrite lookup_merge; intros. specialize (Hm i). destruct (m1 !! i), (m2 !! i); simplify_eq/=; auto using bool_decide_pack. - intros Hm i. specialize (Hm i). rewrite lookup_merge in Hm. destruct (m1 !! i), (m2 !! i); simplify_eq/=; auto; by eapply bool_decide_unpack, Hm. Qed.
imports: Coq(Permutation) stdpp(options)