Really make a newline in generated TPTP
Add a pass that makes min x -> x /= unr
Always make booleans disjoint
Make a toggle for squishy booleans
Fixing min-related translations.
Unsuccessful attempt to discriminate constructor if either is not unreachable.
Remove AEA in favour of DCA, while correctly making CF for nullary constructors

Dimitrios' observation:

[Dan's crazy Axiom (DCA)] :
       min(K xs) /\ not (cf(K xs)) =>  BigOr (min(x_i) /\ not (cf(x_i))

[Another Existing Axiom (AEA) ]:
      min(K xs) /\  (cf xs) => cf(K xs)

Claim:
     DCA => AEA

Let's do what theorem provers do, and see if DCA /\ ~AEA is
 contradictory. What is ~AEA? Well:

       AEA = min(K xs) /\ BigAnd cf(x_i) => cf(K xs)

It's on the form A -> B, and ~(A -> B) = ~(~A \/ B) = A /\ ~B, thus:

      ~AEA = min(K xs) /\ BigAnd cf(x_i) /\ ~cf(K xs)

Now, min(K xs) /\ ~cf(K xs) give us

  (*) BigOr (min(K_i) /\ ~cf(x_i))

Directly from DCA, and we still have the BigAnd cf(x_i) around, so use cf => min:

      /\ BigAnd cf(x_i) /\ BigAnd min(x_i)

But, equation (*) above says that one of these i is

 (**)  ~cf(x_i)

So we have a contradiction. but with one important catch! Consider a
nullary constructor K. We want to say that min(K) => cf(K), and this
before came (vacuously) from AEA, but now we have to add it ourself.

It can be seen it in the derivation above as well, marked (**), that I
pick an i, but if the constructor is nullary, there is no such i to pick.
Make subtheories extendable
Merge together extendable subtheories and minrec
Merge branch 'min-as-not-unr' into extend-subtheory
Make pointers depend on app on min
Remove unnecessary function in Halo.Trim
Change tptp linearisation to equinox's model-printer
Fix renamer and min predicate output
Fix show instance for constraints
Trying to solve constraints, but it's really problematic when you case
on the same variable twice:

    max_concl_ccx = \ (ds_daA :: Max.Nat) (y :: Max.Nat) ->
      case ds_daA of wild_00 {
        __DEFAULT ->
          case y of wild_X5 {
            __DEFAULT ->
              case ds_daA of _ {
                __DEFAULT -> lvl_max_step_ccA; (bad)
                Max.S x ->
                  case y of _ {
                    __DEFAULT -> lvl_max_step_ccB; (bad)
                    Max.S y -> Max.S (max_hyp_ccG x y)
                  }
              };
            Max.Z -> ds_daA
          };
        Max.Z -> y
      }

You get things like this:

    fof(x, definition,
        ! [X,Y] :
            ((min(f_max_concl(c_S(X),Y)) &
              Y != c_unr &
              Y != c_bad &
              Y != c_S(p_0_S(Y)) &
              Y != c_Z &
              c_S(X) != c_unr &
              c_S(X) != c_bad &
              c_S(X) != c_Z) =>
             f_max_concl(c_S(X),Y) = f_lvl_max_step)).

Y can never have such a value.

You also get things like this:

    fof(x, definition,
        ! [Ds,Y] :
            ((min(f_max_concl(Ds,Y)) &
              Y != c_unr &
              Y != c_bad &
              Y != c_Z &
              Ds != c_unr &
              Ds != c_bad &
              Ds != c_Z) =>
             min(Ds))).
    fof(x, definition,
        ! [X,Y] :
            ((min(f_max_concl(c_S(X),Y)) &
              Y != c_unr &
              Y != c_bad &
              Y != c_Z &
              c_S(X) != c_unr &
              c_S(X) != c_bad &
              c_S(X) != c_Z) =>
             min(Y))).

Which is a bit unclear what it really mins
Allow subst of expressions
Fix show instance for Subtheories
Something to make the lifter a bit less grumpy
Mildly fix the lineariser