Definition finstructonfun {X Y : UU} (sx : finstruct X) (sy : finstruct Y) : finstruct (X -> Y) := make_finstruct _ (nelstructonfun sx sy).
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.