fact: Definition union {X : UU} (P : (X → hProp) → hProp) : X → hProp := λ x : X, ∃ A : X → hProp, P A × A x.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Combinatorics.FiniteSequences UniMath.Foundations.NaturalNumbers UniMath.Tactics.EnsureStructuredProofs