fact: Definition power_iterated_shift X n : power_iterated (X -> HProp) n = (power_iterated X n -> HProp) := (nat_iter_succ_r _ _ _)^.
imports: HoTT(Basics Types TruncType) HoTT(PropResizing.PropResizing) HoTT(Spaces.Card Spaces.Nat.Core)