proposition: Lemma hprop_hprop : forall X : Type, IsHProp (IsHProp X).
proof: Proof. intros X p q. apply forall_hprop. intro x. apply forall_hprop. intro y. intros f g. apply (hset_hprop X p). Qed.
imports: Coq.Logic.FunctionalExtensionality