Lemma isaprop_funextemptyStatement : isaprop funextemptyStatement. Proof. unfold funextemptyStatement. apply impred_isaprop; intro X; apply impred_isaprop; intro f; apply impred_isaprop; intro g. generalize g; clear g. generalize f; clear f. change (isaset (X → ∅)). apply impred_isaset; intro x. apply isasetempty. Defined.
Require Import UniMath.Foundations.PartD.