Theorem: Std.RBMap.find?_congr (Etch/Verification/RBMap.lean)

State before:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
k₁ k₂ : α
inst✝ : TransCmp cmp
t : RBMap α β cmp
h : cmp k₁ k₂ = Ordering.eq
⊢ find? t k₁ = find? t k₂
Tactic:
simp [find?, findEntry?_congr _ h]
State after:
no goals