proposition: Lemma listed_have_one_has : forall T (l:list T)(r:hashtools T) (p:T->Prop) (t:T), tools_ok r -> check (fun x => comp r t x) l = true -> listed_have p l -> p t.
proof: Proof. intros T l. induction l. intros. assert (false = true). exact H0. discriminate. intros. assert (bool_or (comp r t0 t) (check (fun x => comp r t0 x) l) = true). assumption. induction (bool_alt (comp r t0 t)). unfold tools_ok in H. pose (H _ _ H3). rewrite e. rewrite listed_have_cons in H1. induction H1; assumption. rewrite H3 in H2. apply IHl with r. assumption. assumption. rewrite listed_have_cons in H1. induction H1; assumption. Qed.