Definition finstructoncompl {X : UU} (x : X) (sx : finstruct X) : finstruct (compl X x). Proof. destruct sx as [n w]. induction n as [| n ]. - exact(fromempty (negstn0 (invweq w x))). - exact(make_finstruct (compl X x) (nelstructoncompl x w)). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.