proposition: Lemma union_hfalse {X : UU} : union (λ _ : X → hProp, hfalse) = (λ _ : X, hfalse).
proof: Proof. apply funextfun ; intros x. apply hPropUnivalence. - apply hinhuniv. intros A. apply (pr1 (pr2 A)). - apply fromempty. Qed.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Combinatorics.FiniteSequences UniMath.Foundations.NaturalNumbers UniMath.Tactics.EnsureStructuredProofs