Theorem: Std.RBSet.findP?_some (Etch/Verification/RBMap.lean)

State before:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
⊢ y ∈ t.val ∧ cut y = Ordering.eq ↔ y ∈ toList t ∧ cut y = Ordering.eq
Tactic:
simp [mem_toList]
State after:
no goals