HasTrChoice 0 A. Proof. intros B sB f. transparent assert (g : (forall a, B a / RelUnit B a)). - intro a. specialize (f a). strip_truncations. exact (class_of _ f). - specialize (qch B _ (RelUnit B) _ _ _ _ g). strip_truncations. apply tr. apply qch. Qed.
Require Import