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