proposition: Lemma hprop_GCH {PR : PropResizing} {FE : Funext} : IsHProp GCH.
proof: 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. now apply InjectsInto_trans with a0. - apply Empty_rec. eapply merely_destruct; try eapply (Cantor_inj a); trivial. now apply InjectsInto_trans with a0. - enough (H = H') as ->; trivial. apply path_ishprop. Qed.
imports: HoTT(TruncType abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Spaces.Nat.Core Spaces.Card)