proposition: Lemma insert_equiv_eq m1 m2 i x : m1 ≡ <[i:=x]> m2 ↔ ∃ x' m2', m1 = <[i:=x']> m2' ∧ x' ≡ x ∧ m2' ≡ m2.
proof: Proof. split; [|by intros (?&?&->&<-&<-)]. intros Hm. assert (is_Some (m1 !! i)) as [x' Hix']. { rewrite Hm, lookup_insert. eauto. } destruct (m2 !! i) as [y|] eqn:?. - exists x', (<[i:=y]> m1). split_and!. + by rewrite insert_insert, insert_id by done. + apply (inj Some). by rewrite <-Hix', Hm, lookup_insert. + by rewrite Hm, insert_insert, insert_id by done. - exists x', (delete i m1). split_and!. + by rewrite insert_delete by done. + apply (inj Some). by rewrite <-Hix', Hm, lookup_insert. + by rewrite Hm, delete_insert by done. Qed.
imports: Coq(Permutation) stdpp(options)