fact: Definition hconj_equiv {X:UU} {A A' B B' : hsubtype X} (e_A : A ≡ A') (e_B : B ≡ B') : (A ∩ B) ≡ (A' ∩ B').
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.WellOrderedSets UniMath.OrderTheory.DCPOs.AlternativeDefinitions.Dcpo