Lemma finite_intersection_case {X : UU} : ∏ (L : Sequence (X → hProp)), finite_intersection L = sumofmaps (λ _ _, htrue) (λ (AB : (X → hProp) × Sequence (X → hProp)) (x : X), pr1 AB x ∧ finite_intersection (pr2 AB) x) (disassembleSequence L). Proof. intros L. apply funextfun ; intros x. apply hPropUnivalence. - intros Hx. induction L as [n L]. induction n as [ | n _] ; simpl. + apply tt. + split. * simple refine (Hx _). * intros m. simple refine (Hx _). - induction L as [n L]. induction n as [ | n _] ; simpl. + intros _ n. apply fromempty. induction (negnatlthn0 _ (pr2 n)). + intros Hx m. change m with (pr1 m,,pr2 m). generalize (pr1 m) (pr2 m) ; clear m ; intros m Hm. induction (natlehchoice _ _ (natlthsntoleh _ _ Hm)) as [Hm' | ->]. * generalize (pr2 Hx (m,,Hm')). unfold dni_lastelement ; simpl. assert (H : Hm = natlthtolths m n Hm' ). { apply (pr2 (natlth m (S n))). } now rewrite H. * assert (H : lastelement = (n,, Hm)). { now apply subtypePath_prop. } rewrite <- H. exact (pr1 Hx). Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Subtypes.