import logic
variable N : Type
variable α : N
variable β₁ : N
check β₁
variable δ : N
check δ
variable δ₁₁ : N
check δ₁₁