Fix for latest Idris

Mostly renaming variables, also new names for dependent pairs.

(By the way, leftDep and rightDep already exist in the library, with the names 'getWitness' and 'getProof'. I expect we should tidy up a few things which can be made neater due to recent fixes in Idris.)