jpm61704 · July 30, 2019 15:16
diff --git a/PiSyn-context.agda b/PiSyn-context.agda

 infix 5 _,_∶_

 data Context : Set where
  ∅ : Context
  _,_∶_ : Context → Id → Expr → Context

 infix 4 _∋_∶_

 data _∋_∶_ : Context → Id → Expr → Set where

  here : ∀ {Γ x A}
       -----------------
       → Γ , x ∶ A ∋ x ∶ A

  there : ∀ {Γ x y A B}
        → x ≢ y
        → Γ ∋ x ∶ A
        -----------------
        → Γ , y ∶ B ∋ x ∶ A