proposition: Lemma epsilon_ind {A:Type} (inh : inhabited A) (P Q : A -> Prop): (ex P ) -> (forall a, P a -> Q a) -> Q (epsilon inh P).
proof: Proof. intros exP P_Q; apply P_Q, epsilon_spec. case exP ;intros x H; exists x;assumption. Qed.