proposition: Lemma get_add_diff : forall T (r:hashtools T) (t:T) a (u:hashtable T), pos_compare a (addr r t) = false -> get a (add r t u) = get a u.
proof: Proof. intros. unfold add. transitivity (get a (put (cons t (get (addr r t) u)) (addr r t) u)). reflexivity. rewrite get_put_diff; try assumption. reflexivity. Qed.