-definition tight_apart: ∀A.∀eq,ap:relation A.Prop
-≝ λA.λeq,ap.∀x,y:A. (¬(ap x y) → eq x y) ∧
-(eq x y → ¬(ap x y)).
+definition tight_apart: ∀A.∀eq,ap:\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 A.Prop
+≝ λA.λeq,ap.∀x,y:A. (\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(ap x y) → eq x y) \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6
+(eq x y → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(ap x y)).