proposition: Lemma natmap_lookup_partial_alter_raw_ne {A} (f : option A → option A) i j l : i ≠ j → mjoin (natmap_partial_alter_raw f i l !! j) = mjoin (l !! j).
proof: Proof. revert i j. induction l; intros [|?] [|?] ?; simpl; repeat case_match; simpl; autorewrite with natmap; auto with congruence. rewrite natmap_lookup_singleton_raw_ne; congruence. Qed.
imports: stdpp(fin_maps mapset) stdpp(options)