Lemma weqexistsnatlehnsn' ( n' : nat ) ( P : nat -> hProp ) : ( hexists ( λ n : nat, ( natleh n ( S n' ) ) × ( P n ) ) ) ≃ hdisj ( hexists ( λ n : nat, ( natleh n n' ) × ( P n ) ) ) ( P ( S n' ) ). Proof. intros. assert ( lg : hexists ( λ n : nat, ( natleh n ( S n' ) ) × ( P n ) ) <-> hdisj ( hexists ( λ n : nat, ( natleh n n' ) × ( P n ) ) ) ( P ( S n' ) ) ). { split. - apply hinhfun. intro t2. destruct t2 as [ n d2 ]. destruct d2 as [ l p ]. destruct ( natlehchoice2 _ _ l ) as [ h | nh ]. + simpl in h. apply ii1. apply hinhpr. split with n. apply ( make_dirprod h p ). + destruct nh. apply ( ii2 p ). - simpl. apply ( @hinhuniv _ ( ishinh _ ) ). intro c. destruct c as [ t | p ]. + generalize t. simpl. apply hinhfun. clear t. intro t. destruct t as [ n d2 ]. destruct d2 as [ l p ]. split with n. split with ( natlehtolehs _ _ l ). apply p. + apply hinhpr. split with ( S n' ). split with ( isreflnatleh _ ). apply p. } apply ( weqimplimpl ( pr1 lg ) ( pr2 lg ) ( pr2 _ ) ( pr2 _ ) ). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.