proposition: Corollary fromnegcoprod_prop {X Y : hProp} : ¬ (X ∨ Y) -> ¬ X ∧ ¬ Y.
proof: Proof. intros n. simpl in *. assert (n' := negf hinhpr n); simpl in n'; clear n. apply fromnegcoprod. assumption. Defined.
imports: UniMath.Foundations.PartD