proposition: Lemma union_hProp {X : UU} : ∏ (P : (X → hProp) → hProp), (∏ (L : (X → hProp) → hProp), (∏ A, L A → P A) → P (union L)) → (∏ A B, P A → P B → P (λ x : X, A x ∨ B x)).
proof: Proof. intros P Hp A B Pa Pb. rewrite <- union_or. apply Hp. intros C. apply hinhuniv. now apply sumofmaps ; intros ->. Qed.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Combinatorics.FiniteSequences UniMath.Foundations.NaturalNumbers UniMath.Tactics.EnsureStructuredProofs