proposition: Lemma iscontraprop1 {X : UU} (is : isaprop X) (x : X) : iscontr X.
proof: Proof. intros. unfold iscontr. split with x. intro t. unfold isofhlevel in is. set (is' := is t x). apply (pr1 is'). Defined.
imports: UniMath.Foundations.PartA