proposition: Theorem success : forall (d:dict) (k:key) (v:data), find k (add k v d) = Some v.
proof: Proof. unfold find, add in |- *; intros d k v; case (Key.eqdec k k); cbn in |- *; tauto. Qed.
imports: Relations List ZArith Arith