* Simplify if combinator in an (unsuccessful) attempt to use it in
  continuations for failT. Still useful though.
* Introduce boolean domains for this simplified version, avoiding full
  numerical domains on conditions.
* Add a SoundConditionalPath constructor to sound' for failT
  continuations. Currently missing hypotheses for soundness, with two
  corresponding admits (and missing proofs for when we transform the
  function in question).
* Simplify argument specifiers for galois_in and GaloisConnection
  instances to avoid extra @ and _ everywhere.
* Introduce unitˣ and optionˣ, even though the second must sometimes be
  inlined due to universe inconsistencies... thanks template poly.
* Introduce notations for universe polymorphic pairs, which I
  temporarily used for optionˣ (didn't work out in the end).