proposition: Lemma binary_intersection_commutative {X : UU} (U V : hsubtype X) : ∏ x : X, (binary_intersection U V) x -> (binary_intersection V U) x.
proof: Proof. intros ? p. exact (transportf _ (iscomm_hconj (U x) (V x)) p). Qed.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Propositions