fact: Definition O_lex_leq_inO_TypeO (O' O : ReflectiveSubuniverse) `{O << O'} `{IsAccRSU O'} `{In (lift_accrsu O') (Type_ O)} : O <<< O'.
imports: HoTT.Basics HoTT.Types HFiber Extensions Limits.Pullback Modality Accessible Localization