failed attempts at proving swapUp0 with new permLeftFn definition
converted \equiv to heterogenous equality. hoping I don't regret this.
got rid of het eq