SHARE
TWEET

Untitled

a guest Sep 22nd, 2017 127 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. Lemma counterexample :
  2.   ~ forall (A : Type) (P : A -> Prop) (Q : Prop), ((forall x, P x) -> Q) -> (exists x, P x -> Q).
  3. Proof.
  4.   intros contra.
  5.   specialize (contra Empty_set (fun _ => False) True (fun _ => I)) as [x _].
  6.   contradiction.
  7. Qed.
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
Top