Theorem: Std.RBNode.Ordered.le_max? (Etch/Verification/RBMap.lean)

State before:
α : Type u_1
cmp : α → α → Ordering
a : α
t : RBNode α
inst✝ : TransCmp cmp
ht : Ordered cmp t
h : RBNode.max? t = some a
x : α
hx : x ∈ t
⊢ x ∈ reverse t
Tactic:
simpa using hx
State after:
no goals