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