proposition: Lemma hprop_hset : forall X : Type, IsHProp (IsHSet X).
proof: Proof. intros X f g. apply functional_extensionality_dep. intro x. apply functional_extensionality_dep. intro y. apply functional_extensionality_dep. intro a. apply functional_extensionality_dep. intro b. apply (hset_hOneType). exact f. Qed.
imports: Coq.Logic.FunctionalExtensionality