proposition: Theorem GCH_injects (X : HSet) : GCH -> InjectsInto X (HN (Build_HSet (Build_HSet (nat + X) -> HProp))).
proof: Proof. intros gch. eapply InjectsInto_trans with (nat + X). - apply tr. exists inr. intros x y. apply path_sum_inr. - apply GCH_injects'; trivial. exists inl. intros x y. apply path_sum_inl. Qed.
imports: HoTT(TruncType ExcludedMiddle abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Spaces.Nat.Core Spaces.Card) HoTT(Equiv.BiInv) HoTT(HIT.unique_choice) HoTT.Sets(Ordinals Hartogs Powers GCH AC)