proposition: Lemma Injection_power_iterated {UA : Univalence} {PR : PropResizing} (X : HSet) n : Injection X (power_iterated X n).
proof: Proof. induction n as [|n IHn]. - reflexivity. - eapply Injection_trans; try apply IHn. apply Injection_power. exact _. Qed.
imports: HoTT(Basics Types TruncType) HoTT(PropResizing.PropResizing) HoTT(Spaces.Card Spaces.Nat.Core)