proposition: Lemma and_hprop : forall P Q : Prop, IsHProp P -> IsHProp Q -> IsHProp (P /\ Q).
proof: Proof. intros. intros p q. destruct p,q. replace p0 with p. - replace q0 with q. + reflexivity. + apply H0. - apply H. Qed.
imports: Coq.Logic.FunctionalExtensionality