Theorem: Std.RBMap.findEntry?_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
⊢ findEntry? t k₁ = findEntry? t k₂
Tactic:
simp [findEntry?, TransCmp.cmp_congr_left' h]
State after:
no goals