a guest Sep 22nd, 2017 127 Never
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).
- intros contra.
- specialize (contra Empty_set (fun _ => False) True (fun _ => I)) as [x _].
RAW Paste Data