proposition: Lemma find_map : forall (B C : Type) (f : B -> C), forall a l, match find a l with | Some b => find a (map (fun xval : A * B => (fst xval, f (snd xval))) l) = Some (f b) | None => find a (map (fun xval : A * B => (fst xval, f (snd xval))) l) = None end.
proof: Proof. fix find_map 5. intros B C f a l; case l; clear l; simpl. reflexivity. intros p l; case p; clear p; intros a1 b1; simpl. case (eq_bool a a1). reflexivity. apply find_map. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)