proposition: Lemma all_have_one_has : forall T (r:hashtools T) (p:T->Prop) (t:T) (u:hashtable T), tools_ok r -> search r t u = true -> all_have p u -> p t.
proof: Proof. intros. assert (listed_have p (get (addr r t) u)). apply H1. unfold search in H0. apply listed_have_one_has with T (get (addr r t) u) r. assumption. assumption. assumption. Qed.