Lemma hconjtohdisj (P Q : UU) (R : hProp) : (P ⇒ R) ∧ (Q ⇒ R) -> (P ∨ Q) ⇒ R. Proof. intros X0. assert (s1: hdisj P Q -> R). { intro X1. assert (s2: coprod P Q -> R). { intro X2. induction X2 as [ XP | XQ ]. - apply X0. apply XP. - apply (pr2 X0). apply XQ. } apply (hinhuniv s2). apply X1. } unfold himpl. simpl. apply s1. Defined.