Lemma iscontrtildehProp : iscontr tildehProp. Proof. split with (tpair _ htrue tt). intro tP. induction tP as [ P p ]. apply (invmaponpathsincl _ (isinclpr1 (λ P : hProp, P) (λ P, pr2 P))). simpl. apply hPropUnivalence. apply (λ x, tt). intro t. apply p. Defined.