lower'2@{i i' j j'} {A : Type@{i}} {B : A -> Type@{i'}} (f : forall x : Lift'@{i j} A, Lift'@{i' j'} (B (lower' x))) : forall x : A, B x := f.
From HoTT Require Import Basics.Overture Basics.PathGroupoids.