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

State before:
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
x : α
t : RBMap α β cmp
⊢ contains t x = true ↔ ∃ v, find? t x = some v
Tactic:
simp [contains_iff_findEntry?, find?, and_comm, exists_comm]
State after:
no goals