Just a universally quantified hypotesis in coq proof
Another hard goal (for me, of course) is the following:
Goal ~(forall P Q: nat -> Prop,
(exists x, P x) /\ (exists x, Q x) ->
(exists x, P x /\ Q x)).
Proof.
I absolutely have no idea of what could I do. If I introduce something, I
get a universal quantifier in the hypotesis, and then I can't do anything
with it.
I suppose that it exists a standard way for managing such kind of
situations, but I was not able to find it out.
No comments:
Post a Comment