Lemma hinhuniv2' {P X Y : UU} : isaprop P → (X → Y → P) → (∥ X ∥ → ∥ Y ∥ → P). Proof. intros HP Hxy. apply (hinhuniv2 (P := make_hProp _ HP)). exact Hxy. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Subtypes.