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

Thm* i,j:. i=j