proposition: Lemma alter_equiv_eq (f : A → A) (m1 m2 : M A) i : Proper ((≡) ==> (≡)) f → (∀ x1 x2, x1 ≡ f x2 → ∃ x2', x1 = f x2' ∧ x2' ≡ x2) → m1 ≡ alter f i m2 ↔ ∃ m2', m1 = alter f i m2' ∧ m2' ≡ m2.
proof: Proof. intros ? Hf. apply (partial_alter_equiv_eq _ _ _ _ _). intros mx1 [x2|]; simpl. - intros (x2'&->&?)%(inj _)%Hf. exists (Some x2'). by repeat constructor. - intros ->%None_equiv_eq. by exists None. Qed.
imports: Coq(Permutation) stdpp(options)