implicit.agda

open import Agda.Builtin.Bool

data ⊥ : Set where
record ⊤ : Set where

isTrue : Bool → Set
isTrue true = ⊤
isTrue false = ⊥

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}

variable
  n m p : ℕ

_≤_ : ℕ → ℕ → Bool
zero ≤ m = true
suc n ≤ zero = false
suc n ≤ suc m = n ≤ m

data _⊔_≡_ : ℕ → ℕ → ℕ → Set where
  m≥⊔n≡m : {_ : isTrue (n ≤ m)}
         ---------
        → m ⊔ n ≡ m

  m≤⊔n≡n : {_ : isTrue (m ≤ n)}
         ---------
        → m ⊔ n ≡ n


_ : 0 ⊔ 4 ≡ 4
_ = m≤⊔n≡n

meme.agda

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}

variable
  n m p : ℕ

data _≤_ : ℕ → ℕ → Set where
  z≤n : zero ≤ n

  s≤s : m ≤ n
      -------------
    → suc m ≤ suc n

data _⊔_≡_ : ℕ → ℕ → ℕ → Set where
  m≥⊔n≡m : n ≤ m
         ---------
        → m ⊔ n ≡ m

  m≤⊔n≡n : m ≤ n
         ---------
        → m ⊔ n ≡ n

infix 4 _≤_

data Formula : ℕ → Set where
  var : (n : ℕ) → n ≤ m → Formula m
  ∩_ : Formula m → Formula (suc m)
  ∪_ : Formula m → Formula (suc m)
  α : Formula m → Formula n → (m ⊔ n ≡ p) → Formula p
  ν : Formula m → Formula n → (m ⊔ n ≡ p) → Formula p

x : Formula zero
x = var zero z≤n

∩xx : Formula (suc zero)
∩xx = ∩ (var zero z≤n)

xα∩xx : Formula (suc zero)
xα∩xx = α x ∩xx (m≤⊔n≡n z≤n)

∩xxαx : Formula (suc zero)
∩xxαx = α ∩xx x (m≥⊔n≡m z≤n)

∩xxα∩xx : Formula (suc zero)
∩xxα∩xx = α ∩xx ∩xx (m≥⊔n≡m (s≤s z≤n))