Lemma finite_intersection_append {X : UU} : ∏ (A : X → hProp) (L : Sequence (X → hProp)), finite_intersection (append L A) = (λ x : X, A x ∧ finite_intersection L x). Proof. intros A L. rewrite finite_intersection_case. simpl. rewrite append_vec_compute_2. apply funextfun ; intro x. apply maponpaths. apply map_on_two_paths. - induction L as [n L] ; simpl. apply maponpaths. apply funextfun ; intro m. simpl. rewrite <- replace_dni_last. apply append_vec_compute_1. - reflexivity. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Subtypes.