proposition: Theorem make_impl_map : forall (A B: Type) (eval : A -> Prop) (eval' : A*B -> Prop) (l : list (A*B)) r (EVAL : forall x, eval' x <-> eval (fst x)), make_impl eval' l r <-> make_impl eval (List.map fst l) r.
proof: Proof. intros A B eval eval' l; induction l as [| a l IH]; simpl. - tauto. - intros r EVAL. rewrite EVAL. rewrite IH. + tauto. + auto. Qed.
imports: List