Theorem isapropiscontr (T : UU) : isaprop (iscontr T). Proof. intros. unfold isaprop. unfold isofhlevel. intros x x'. assert (is : iscontr(iscontr T)). apply iscontriscontr. apply x. assert (is2 : isaprop (iscontr T)) by apply (isapropifcontr is). apply (is2 x x'). Defined.