proposition: Lemma injective_power_inj `{PropResizing} {ua : Univalence} (C : Type@{i}) : IsInjective (@power_inj _ C).
proof: Proof. intros p p'. unfold power_inj. intros q. apply path_forall. intros a. apply path_iff_hprop; intros Ha. - eapply equiv_resize_hprop. change ((fun a => Build_HProp (resize_hprop (p' a))) a). rewrite <- q. apply equiv_resize_hprop. apply Ha. - eapply equiv_resize_hprop. change ((fun a => Build_HProp (resize_hprop (p a))) a). rewrite q. apply equiv_resize_hprop. apply Ha. Qed.
imports: HoTT(TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra HSet) HoTT(PropResizing.PropResizing) HoTT(Spaces.Card) HoTT.Sets(Ordinals Powers)