proposition: Lemma U_T : forall A, T A -> U A.
proof: Proof. intros A H; unfold T, U in *. assert (Hi : inhabited ((inhabited epsilon) -> A)). apply choice; auto. intros [Hi]; constructor; intuition. destruct Hi as [Hi]; constructor; apply Hi. clear; unfold epsilon. apply (choice Type); intros A; apply choice; intros B; apply choice. intros [x Hx]; constructor; eauto. Qed.