proposition: Lemma find_app : forall (B : Type) a (l1 l2 : list (A * B)), find a (l1 ++ l2) = if mem_bool a (map (fun st => fst st) l1) then find a l1 else find a l2.
proof: Proof. fix find_app 3. intros B a l1; case l1; clear l1; simpl. intros l2; reflexivity. intros p l1 l2; case p; clear p; intros a1 b1; simpl. case (eq_bool a a1); simpl. reflexivity. apply find_app. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)