Theorem: Std.RBMap.findD_insert_of_ne (Etch/Verification/RBMap.lean)

State before:
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
k' k : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
h : cmp k' k ≠ Ordering.eq
d : β
⊢ findD (insert t k v) k' d = findD t k' d
Tactic:
simp [findD_insert, h]
State after:
no goals