なんか自分のレベルをさらけだしてるみたいで嫌だが

めも

~$ coqtop

Welcome to Coq 8.0pl2 (Jan 2005)
Coq < Section Predicate_calculus.
Coq < Variable D:Set.

D is assumed
Coq < Variable P:D->Prop.

P is assumed
Coq < Variable Q:Prop.

Q is assumed
Coq < Goal (Q-> forall x:D, P x) -> (forall y:D, Q->P y).

1 subgoal
  D : Set

  P : D -> Prop

  Q : Prop

  ============================

   (Q -> forall x : D, P x) -> forall y : D, Q -> P y
Unnamed_thm < auto.

Proof completed.