fact: Definition inequality_to_isolation {X : UU} (x : X) (i : isisolated X x) (y : X) : x != y -> isolation x i y := pair_falsehood (to_ComplementaryPair (i y)).
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Tactics