proposition: 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: 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.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Combinatorics.FiniteSequences UniMath.Foundations.NaturalNumbers UniMath.Tactics.EnsureStructuredProofs