fact: Definition map_relation `{∀ A, Lookup K A (M A)} {A B} (R : A → B → Prop) (P : A → Prop) (Q : B → Prop) (m1 : M A) (m2 : M B) : Prop := ∀ i, option_relation R P Q (m1 !! i) (m2 !! i).
imports: Coq(Permutation) stdpp(options)