fact: Definition find (k : key) (d : dict) : option data := let (t, Ht) := d in match occ_dec k t Ht with | inleft s => let (v, _) := s in Some v | inright _ => None (A:=data) end.
imports: Relations List ZArith Arith