Lemma isaprop_funcontrStatement : isaprop funcontrStatement. Proof. unfold funcontrStatement. apply impred_isaprop; intro X; apply impred_isaprop; intro P; apply impred_isaprop; intros _. apply isapropiscontr. Defined.
Require Import UniMath.Foundations.PartD.