Inconsistent lemma statements and names: Some_equiv_eq vs the equivalent lemma on dist
Some_equiv_eq:
∀ {A : Type} {H : Equiv A} (mx : option A) (y : A), mx ≡ Some y ↔ (∃ y' : A, mx = Some y' ∧ y' ≡ y)
vs
dist_Some_inv_l':
∀ {A : ofe} (n : nat) (my : option A) (x : A),
Some x ≡{n}≡ my → ∃ x' : A, Some x' = my ∧ x ≡{n}≡ x'
dist_Some_inv_r':
∀ {A : ofe} (n : nat) (mx : option A) (y : A),
mx ≡{n}≡ Some y → ∃ y' : A, mx = Some y' ∧ y ≡{n}≡ y'