misc
{-# OPTIONS --cubical #-} module agda.dbi where open import Cubical.Foundations.Prelude open import Cubical.Data.Nat
data Term : Set where var : ℕ → Term lam : Term → Term app : Term → Term → Term example₁ : Term example₁ = lam {-x-} (lam {-y-} (app (var {-x-} 1) (var {-y-} 0)))