proposition: Lemma finite_intersection_1 {X : UU} : ∏ (A : X → hProp), finite_intersection (singletonSequence A) = A.
proof: Proof. intros A. apply funextfun ; intros x. apply hPropUnivalence. - intros H. simple refine (H _). now exists 0. - intros Lx m. exact Lx. Qed.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Combinatorics.FiniteSequences UniMath.Foundations.NaturalNumbers UniMath.Tactics.EnsureStructuredProofs