proposition: Lemma mem_bool_app : forall a l1 l2, mem_bool a (l1 ++ l2) = orb (mem_bool a l1) (mem_bool a l2).
proof: Proof. fix mem_bool_app 2. intros a l1; case l1; clear l1. intros l2; reflexivity. simpl; intros a1 l1 l2; rewrite mem_bool_app; rewrite orb_assoc; reflexivity. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)