proposition: Lemma mem_bool_ok : forall a l, match mem_bool a l with true => mem a l | false => ~mem a l end.
proof: Proof. fix mem_bool_ok 2. intros a l; case l; simpl. intro F; assumption. intros b k; generalize (eq_bool_ok a b); case (eq_bool a b). intro a_eq_b; left; assumption. intro a_diff_b; simpl; generalize (mem_bool_ok a k); case (mem_bool a k). intro a_in_k; right; assumption. intros a_not_in_k a_in_bk; case a_in_bk; clear a_in_bk. exact a_diff_b. exact a_not_in_k. Defined.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)