Theorem: Option.coe_part_eq_some (Etch/Verification/Misc.lean)

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
x : Option α
y : α
⊢ ↑x = Part.some y ↔ x = some y
Tactic:
simp [Part.eq_some_iff]
State after:
no goals