proposition: Lemma all_have_add : forall T (r:hashtools T) (p:T->Prop) (t:T)(u:hashtable T), all_have p (add r t u) = (p t /\ all_have p u).
proof: Proof. intros. apply iff_eq; intros. apply conj. pose (H (addr r t)). assert (listed_have p (get (addr r t) (add r t u))). assumption. rewrite get_add_same in H0. rewrite listed_have_cons in H0. induction H0; assumption. apply pos_compare_refl. unfold all_have. intro a. induction (bool_alt (pos_compare a (addr r t))). assert (get a (add r t u) = cons t (get a u)). rewrite get_add_same; try assumption. reflexivity. pose (H a). assert (listed_have p (get a (add r t u))). assumption. rewrite H1 in H2. rewrite listed_have_cons in H2. induction H2; assumption. assert (get a u = get a (add r t u)). rewrite get_add_diff; try assumption. reflexivity. rewrite H1. exact (H a). unfold all_have. intro a. induction (bool_alt (pos_compare a (addr r t))). rewrite get_add_same; try assumption. rewrite listed_have_cons. apply conj. induction H; assumption. induction H. apply H1. rewrite get_add_diff. induction H. apply H1. assumption. Qed.