Refactoring uses of with

[jamesmckinna]

Cf. #1937

As well as removing 'redundant' uses of with, it seems worth flagging as a separate issue the need/desire to exploit the (idiomatics of the) extended capabilities of with notation throughout the library. Specifically:

• use of nested with esp. in conjunction with the next idiom, irrefutable with, building up a cascade of dependent inversions until the final RHS proof term may be assembled from the resulting pieces;
• use of 'irrefutable' with: with <pat> ← <exp> = ... which avoids having to uncouple the sub-expression <exp> from the single matching clause ... | <pat> = ... with which the definition then proceeds; there are three distinguished special cases of this, according to the form of <pat>:

• () or more generally, <constructor> (<constructor>... ()...), as a (convenient?) drop-in replacement for more explicit appeals to ⊥-elim or Relation.Nullary.Negation.Core.contradiction;
• refl: such uses seem strictly to extend the capability of rewrite <exp> for an <exp> of type s ≡ t;
• <pat1> , <pat2> , ... , <patn> (and record constructors more generally) for extended/nested Σ-types; the advantages being that parentheses around the pattern are frequently redundant clutter, but also that such uses may often also permit simplification in the form of replacing the use of an irrefutable with pattern with a let <pat1> , <pat2> , ... , <patn> = <exp> in ... binding instead;

• the use of with <exp> in <eq>: this is perhaps more controversial, given the ongoing saga of this notation not precisely offering a drop-in replacement for the hoped-to-be-deprecated inspect idiom; nevertheless, all uses of inspect have been successfully removed from the library, so the use of this extended form is encouraged where possible;

Other features/idioms as they arise... with the proposal that at some point (v2.1? v3.0?) we systematically weed out the redundant uses of with and refactor to take advantage of the above.