proposition: Lemma forall_hprop : forall (A : Type) (P : A -> Prop), (forall x:A, IsHProp (P x)) -> IsHProp (forall x:A, P x).
proof: Proof. intros A P H p q. apply functional_extensionality_dep. intro x. apply H. Qed.
imports: Coq.Logic.FunctionalExtensionality