proposition: Lemma isaprop_funextcontrStatement : isaprop funextcontrStatement.
proof: Proof. unfold funextcontrStatement. apply impred_isaprop; intro T; apply impred_isaprop; intro P; apply impred_isaprop; intro g. apply isapropiscontr. Defined.
imports: UniMath.Foundations.PartD