Def i=j == if i=jtrue; false fi

Thm* i,j:. i=j