proposition: Lemma finite_intersection_htrue {X : UU} : finite_intersection nil = (λ _ : X, htrue).
proof: Proof. apply funextfun ; intros x. apply hPropUnivalence. - intros _. apply tt. - intros _ m. generalize (pr1 m) (pr2 m). intros m' Hm. apply fromempty. revert Hm. apply negnatlthn0. Qed.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Combinatorics.FiniteSequences UniMath.Foundations.NaturalNumbers UniMath.Tactics.EnsureStructuredProofs