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)).
Require Import UniMath.MoreFoundations.Tactics.