{PR : PropResizing} {FE : Funext} : IsHProp GCH. Proof. repeat (nrapply istrunc_forall; intros). apply hprop_allpath. intros [H|H] [H'|H']. - enough (H = H') as ->; trivial. apply path_ishprop. - apply Empty_rec. eapply merely_destruct; try eapply (Cantor_inj a); trivial. by apply InjectsInto_trans with a0. - apply Empty_rec. eapply merely_destruct; try eapply (Cantor_inj a); trivial. by apply InjectsInto_trans with a0. - enough (H = H') as ->; trivial. apply path_ishprop. Qed.
From HoTT Require Import TruncType abstract_algebra. From HoTT Require Import Universes.Smallness. From HoTT Require Import Spaces.Nat.Core Spaces.Card.