proposition: Lemma find_not_found : forall (B : Type) (a a' : A) (b : B) (l : list (A * B)), find a l = None -> eq_bool a a' = true -> ~In (a',b) l.
proof: Proof. fix find_not_found 5. intros B a a' b l; case l; clear l. intros _ _ Abs; contradiction. intros p l; case p; clear p; intros a1 b1; simpl. case_eq (eq_bool a a1). intros _ Abs; discriminate. intros a_diff_a1 F a_eq_a' H; case H; clear H; intro H. injection H; clear H; intros; subst a1 b1. rewrite a_eq_a' in a_diff_a1; discriminate. apply (find_not_found _ _ _ _ _ F a_eq_a' H). Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)