proposition: Lemma constructive_indefinite_description_and_small_drinker_imp_epsilon : SmallDrinker'sParadox -> ConstructiveIndefiniteDescription -> EpsilonStatement.
proof: Proof. intros Drinkers D_epsilon A P Inh; apply D_epsilon; apply Drinkers; assumption. Qed.
imports: RelationClasses Logic