proposition: Lemma get_add_same : forall T (r:hashtools T) (t:T) a (u:hashtable T), pos_compare a (addr r t) = true -> get a (add r t u) = cons t (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_same; try assumption. assert (a = addr r t). apply pos_compare_eq; assumption. rewrite H0; reflexivity. Qed.