proposition: Theorem isapropiscontr (T : UU) : isaprop (iscontr T).
proof: 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.
imports: UniMath.Foundations.PartC