Lemma weqforallnatlehnsn' ( n' : nat ) ( F : nat -> hProp ) : ( ∏ n : nat , natleh n ( S n' ) -> F n ) ≃ ( ∏ n : nat , natleh n n' -> F n ) × ( F ( S n' ) ). Proof. intros. assert ( lg : ( ∏ n : nat , natleh n ( S n' ) -> F n ) <-> ( ∏ n : nat , natleh n n' -> F n ) × ( F ( S n' ) ) ). { split. - intro f. apply ( make_dirprod ( λ n, λ l, ( f n ( natlehtolehs _ _ l ) ) ) ( f ( S n' ) ( isreflnatleh _ ) ) ). - intro d2. intro n. intro l. destruct ( natlehchoice2 _ _ l ) as [ h | e ]. + simpl in h. apply ( pr1 d2 n h ). + destruct d2 as [ f2 d2 ]. rewrite e. apply d2. } assert ( is1 : isaprop ( ∏ n : nat , natleh n ( S n' ) -> F n ) ). { apply impred. intro n. apply impred. intro l. apply ( pr2 ( F n ) ). } assert ( is2 : isaprop ( ( ∏ n : nat , natleh n n' -> F n ) × ( F ( S n' ) ) ) ). { apply isapropdirprod. - apply impred. intro n. apply impred. intro l. apply ( pr2 ( F n ) ). - apply ( pr2 ( F ( S n' ) ) ). } apply ( weqimplimpl ( pr1 lg ) ( pr2 lg ) is1 is2 ). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.