Internal representation of `if _ then _ else _`

It often happens (particularly during function evaluation) that we have if _ then _ else _ patterns, which are encoded in Kore as

(P ∧ A) ∨ (¬P ∧ B)  // if P then A else B

which evaluates the predicate P twice. We would prefer to have something like an alias,

// cond-itional, in homage to Lisp
alias \cond(P, A, B) := (P ∧ A) ∨ (¬P ∧ B)

with some recognition that the predicate P need only be evaluated once.
Further, in a chain of conditions,

\cond(P, A, \cond(P', B, C))

if P = ⊤, then we never need to consider P'.

I would like to introduce an internal TermLike node,

-- represents a nested sequence of conditionals as above
newtype Cond variable = Cond { getCond :: Seq (Predicate variable, TermLike variable) }

data TermLikeF variable
    = ...
    | CondF (Cond variable)

(Presently, using a Predicate in this place would introduce a circular dependency, but it is not complicated to refactor that dependency away.)

Start by tracing the TermLikeF definition and the Predicate dependency mentioned in the issue, then inspect how the existing conjunction/disjunction encoding evaluates conditionals. The change is complete when nested conditionals can be represented by Cond without a circular dependency and can avoid reevaluating predicates or later branches when an earlier predicate is true.