4648̣.agda

module 4648̣ where

open import Agda.Builtin.List using (List ; _∷_)

a∷as:ListA : ∀ {A : Set} → ∀ {a : A} → ∀ {as : List A} → List A
a∷as:ListA {X} {x} {xs} = x ∷ xs

variable
  I : Set

postulate
  σ : I
  Γ : List I

σ∷Γ:ListI : List I
σ∷Γ:ListI = σ ∷ Γ

variable
  τ : I
  Δ : List I

-- fails: Generalizable variable σ is not supported here
τ∷Δ:ListI₁ : List I
τ∷Δ:ListI₁ = τ ∷ Δ

-- fails: Generalizable variable σ is not supported here
τ∷Δ:ListI₂ : List I
τ∷Δ:ListI₂ = a∷as:ListA {I} {τ} {Δ}