added direction to instantiation so when doing ?f x =?= c y with FO it will try x =?= y and not y =?= x
added a complicated function to remove etas added by instantiation. will change in a future...