Есть ли какая-то тактика для работы с предусловиями с "и"?

Question

Моя цель как ниже. Есть ли какая-то тактика для решения этих тривиальных задач?

Goal forall A (x : A) P Q,
  (forall y, P y /\ Q y) ->
  Q x.
Proof.
  intros. intuition. auto.
Abort.

(* a more complex version *)
Goal forall A (x : A) P Q R,
  (forall y, R -> P y /\ Q y) ->
  R ->
  Q x.
Proof.
  intros. intuition. auto.
Abort.

Answer 1

Тактика intuition не работает, потому что эта тактика разработана для логики высказываний (т.е. она не является квантификатором в forall y, R -> ... Для этого есть другая тактика, она называется firstorder, Попытайся!