proposition: Lemma pred_epsilon_weaken : forall A {IA:Inhab A} (P Q : A->Prop), (exists x, P x) -> (forall x, P x -> Q x) -> Q (epsilon P).
proof: Proof. Proof using. introv E M. apply M. apply* pred_epsilon. Qed.
imports: TLC(LibTactics LibLogic LibRelation)