One more: "I'm not sure if there should be a case for the constructor refl, because I get stuck when trying to solve the following unification problems"

Reduce.agda

open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.String
open import Data.Bool
open import Data.Unit

record Level : Set where
  constructor level
  field
    vars : Bool
    lams : Bool
    lets : Bool

infixl 6 _⊔_
_⊔_ : Level → Level → Level
level v₁ lm₁ lt₁ ⊔ level v₂ lm₂ lt₂ = level (v₁ ∨ v₂) (lm₁ ∨ lm₂) (lt₁ ∨ lt₂)

pattern Core = level false false false
pattern Vars = level true false false

data Term : Level -> Set where
    S   : Term Core
    K   : Term Core
    I   : Term Core
    App : ∀ {a b c} → Term a → Term b → a ⊔ b ≡ c → Term c
    Var : String → Term Vars
    Lam : ∀ {a b} → String → Term a → record a {lams = true} ≡ b → Term b
    Let : ∀ {a b c} → String → Term a → Term b → record (a ⊔ b) {lets = true} ≡ c → Term c

infixr 1 _$₀_
pattern _$₀_ a b = App {a = Core} {b = Core} a b refl

reduce : Term Core → Term Core
reduce (I $₀ x) = x
reduce (K $₀ x $₀ _) = x
reduce (S $₀ x $₀ y $₀ z) = x $₀ y $₀ (x $₀ z)
reduce (f $₀ x) = reduce f $₀ x
reduce t = t -- commenting this line still gives:
{-
I'm not sure if there should be a case for the constructor refl,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  level vars lams lets ⊔ level vars₁ lams₁ lets₁ ≟ level false false
                                                   false
when checking the definition of reduce
-}