`{IsAccRSU O} `{In (lift_accrsu O) (Type_ O)} : Lex O. Proof. apply (O_lex_leq_inO_TypeO O O). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Limits.Pullback Factorization Truncations.Core. Require Import Modality Accessible Modalities.Localization Descent Separated.