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