proposition: Lemma map_agree_Some_r {A} (m1 m2 : M A) i x: map_agree m1 m2 → m2 !! i = Some x → m1 !! i = Some x ∨ m1 !! i = None.
proof: Proof. rewrite (symmetry_iff map_agree). apply map_agree_Some_l. Qed.
imports: Coq(Permutation) stdpp(options)