Lemma isaprop_isProofIrrelevant X : isaprop (isProofIrrelevant X). Proof. intros. apply invproofirrelevance. intros i j. apply funextsec; intro x; apply funextsec; intro y. generalize (i x y) as p; generalize (j x y) as q; intros. apply isProofIrrelevant_paths. assumption. Defined.