Lemma weqforallnatlehn0 ( F : nat -> hProp ) : ( ∏ n : nat , natleh n 0 -> F n ) ≃ ( F 0 ). Proof. intros. assert ( lg : ( ∏ n : nat , natleh n 0 -> F n ) <-> ( F 0 ) ). { split. - intro f. apply ( f 0 ( isreflnatleh 0 ) ). - intros f0 n l. set ( e := natleh0tois0 l ). rewrite e. apply f0. } assert ( is1 : isaprop ( ∏ n : nat , natleh n 0 -> F n ) ). { apply impred. intro n. apply impred. intro l. apply ( pr2 ( F n ) ). } apply ( weqimplimpl ( pr1 lg ) ( pr2 lg ) is1 ( pr2 ( F 0 ) ) ). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.