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. intros P Hp A B Pa Pb. rewrite <- union_or. apply Hp. intros C. apply hinhuniv. now apply sumofmaps ; intros ->. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Subtypes.