proposition: Lemma infinite_power_iterated {UA : Univalence} {PR : PropResizing} (X : HSet) n : infinite X -> infinite (power_iterated X n).
proof: Proof. intros H. eapply infinite_inject; try apply H. apply Injection_power_iterated. Qed.
imports: HoTT(Basics Types TruncType) HoTT(PropResizing.PropResizing) HoTT(Spaces.Card Spaces.Nat.Core)