Lemma hdisjtoimpl {P : UU} {Q : hProp} : P ∨ Q -> ¬ P -> Q. Proof. assert (int : isaprop (¬ P -> Q)). { apply impred. intro. apply (pr2 Q). } simpl. apply (@hinhuniv _ (make_hProp _ int)). simpl. intro pq. induction pq as [ p | q ]. - intro np. induction (np p). - intro np. apply q. Defined.