Definition isofnelcompl {X : UU} {n : nat} (x : X) (sx : isofnel (S n) X) : isofnel n (compl X x) := hinhfun (nelstructoncompl x) sx.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.