Lemma finite_intersection_hProp {X : UU} : ∏ (P : (X → hProp) → hProp), (∏ (L : Sequence (X → hProp)), (∏ n, P (L n)) → P (finite_intersection L)) <-> (P (λ _, htrue) × (∏ A B, P A → P B → P (λ x : X, A x ∧ B x))). Proof. intros P. split. - split. + rewrite <- finite_intersection_htrue. apply X0. intros n. induction (negnatlthn0 _ (pr2 n)). + intros A B Pa Pb. rewrite <- finite_intersection_and. apply X0. intros n. change n with (pr1 n,,pr2 n). generalize (pr1 n) (pr2 n) ; clear n ; intros n Hn. now induction n as [ | n _] ; simpl. - intros Hp. apply (Sequence_rect (P := λ L : Sequence (X → hProp), (∏ n : stn (length L), P (L n)) → P (finite_intersection L))). + intros _. rewrite finite_intersection_htrue. exact (pr1 Hp). + intros L A IHl Hl. rewrite finite_intersection_append. apply (pr2 Hp). * rewrite <- (append_vec_compute_2 L A). now apply Hl. * apply IHl. intros n. rewrite <- (append_vec_compute_1 L A). apply Hl. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Subtypes.