proposition: Theorem constructive_indefinite_description_and_small_drinker_iff_epsilon : (SmallDrinker'sParadox * ConstructiveIndefiniteDescription -> EpsilonStatement) * (EpsilonStatement -> SmallDrinker'sParadox * ConstructiveIndefiniteDescription).
proof: Proof. intuition auto using epsilon_imp_constructive_indefinite_description, constructive_indefinite_description_and_small_drinker_imp_epsilon, epsilon_imp_small_drinker. Qed.
imports: RelationClasses Logic