To progress in that proof, you will have to exhibit an instance of P
and an instance of Q
such that your hypothesis produces a contradiction.
A simple way to go is to use:
P : fun x => x = 0
Q : fun x => x = 1
In order to work with the hypothesis introduced, you might want to use the tactic specialize
:
Goal ~(forall P Q : nat -> Prop,
(exists x, P x) /\ (exists x, Q x) ->
(exists x, P x /\ Q x)).
Proof.
intro H.
specialize (H (fun x => x = 0) (fun x => x = 1)).
It allows you to apply one of your hypothesis on some input (when the hypothesis is a function). From now on, you should be able to derive a contradiction easily.
Alternatively to specialize
, you can also do:
pose proof (H (fun x => x = 0) (fun x => x = 1)) as Happlied.
Which will conserve H and give you another term Happlied
(you choose the name) for the application.