Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- Lemma counterexample :
- ~ forall (A : Type) (P : A -> Prop) (Q : Prop), ((forall x, P x) -> Q) -> (exists x, P x -> Q).
- Proof.
- intros contra.
- specialize (contra Empty_set (fun _ => False) True (fun _ => I)) as [x _].
- contradiction.
- Qed.
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
