proposition: Lemma find_map2 : forall (B C : Type) (f : (A * B) -> C), forall a l, match find a l with | Some b => exists a', eqA a a' /\ find a (map (fun xval : A * B => (fst xval, f xval)) l) = Some (f (a',b)) | None => find a (map (fun xval : A * B => (fst xval, f xval)) l) = None end.
proof: Proof. intros B C f a l; induction l as [ | [a1 b1] l]; simpl; trivial. generalize (eq_bool_ok a a1); destruct (eq_bool a a1). intro a_eq_a1; exists a1; split; trivial. trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)