Lemma weqexistsnatlehn0 ( P : nat -> hProp ) : ( hexists ( λ n : nat, ( natleh n 0 ) × ( P n ) ) ) ≃ P 0. Proof. assert ( lg : hexists ( λ n : nat, ( natleh n 0 ) × ( P n ) ) <-> P 0 ). { split. - simpl. apply ( @hinhuniv _ ( P 0 ) ). intro t2. destruct t2 as [ n d2 ]. destruct d2 as [ l p ]. set ( e := natleh0tois0 l ). clearbody e. destruct e. apply p. - intro p. apply hinhpr. split with 0. split with ( isreflnatleh 0 ). 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.