proposition: Lemma small_drinker_paradox : forall `{Inhab A} (P : A -> Prop), exists x, (exists x, P x) -> P x.
proof: Proof. Proof using. intros A I P. destruct (prop_inv (exists x, P x)). destruct H. exists x. auto. exists (arbitrary (A:=A)). auto_false. Qed.
imports: TLC(LibTactics)