Definition preweq ( X : UU ) (is: isfinite X): isofnel (carddneg X is) X. Proof. intros X is X0. set (c:= carddneg X is). set (dnw:= pr2 (isfiniteimplisfinite0 X is)). simpl in dnw. change (pr1 nat (λ n : nat, isofnel0 n X) (isfiniteimplisfinite0 X is)) with c in dnw. assert (f: dirprod (finitestruct X) (dneg (weq (stn c) X)) -> weq (stn c) X). intro H. destruct H as [ t x ]. destruct t as [ t x0 ]. assert (dw: dneg ((stn t) ≃ (stn c))). set (ff:= fun ab:dirprod (weq (stn t) X)(weq (stn c) X) => weqcomp _ _ _ (pr1 ab) (invweq (pr2 ab))). apply (dnegf _ _ ff (inhdnegand _ _ (todneg _ x0) x)). assert (e:t = c). apply (stnsdnegweqtoeq _ _ dw). clear dnw. destruct e. assumption. unfold isofnel. apply (hinhfun _ _ f (hinhand (finitestruct X) _ is (hinhpr dnw))). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.