れんしう

∃a∀b[P(a, b)] → ∀b∃a[P(a, b)]

Lemma exists_forall : forall (A:Type)(P: A -> A -> Prop),
  (exists a:A, forall b:A, P a b) -> (forall b:A, exists a:A, P a b).
Proof.
  intros A P H1 a.
  elim H1.
  intros x H2.
  exists x.
  apply H2.
Qed.