proposition: Lemma isaprop_isweqtoforallpathsStatement : isaprop isweqtoforallpathsStatement.
proof: Proof. unfold isweqtoforallpathsStatement. apply impred_isaprop; intro T; apply impred_isaprop; intro P; apply impred_isaprop; intro f; apply impred_isaprop; intro g. apply isapropisweq. Defined.
imports: UniMath.Foundations.PartD