Lemma iscontrloopsifisaset (X : UU) : (isaset X) -> (∏ x : X, iscontr (x = x)). Proof. intros X0 x. unfold isaset in X0. unfold isofhlevel in X0. change (∏ (x x' : X) (x0 x'0 : x = x'), iscontr (x0 = x'0)) with (∏ (x x' : X), isaprop (x = x')) in X0. apply (iscontraprop1 (X0 x x) (idpath x)). Defined.