proposition: Lemma isaprop_funextemptyStatement : isaprop funextemptyStatement.
proof: 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.
imports: UniMath.Foundations.PartD