def termContext : Lean.ParserDescr

Equations

• termContext = Lean.ParserDescr.node `termContext 1024 (Lean.ParserDescr.symbol "context")

def context_terms : context → Finset ℕ

Equations

• context_terms [] = ∅
• context_terms ((x_1, snd) :: Γ') = {x_1} ∪ context_terms Γ'

def in_context (x : ℕ) : context → Prop

Equations

• in_context x [] = False
• in_context x (b :: m) = (x = b.1 ∨ in_context x m)

theorem context_terms_iff_in_list (x : ℕ) (Γ : context) : x ∈ context_terms Γ ↔ in_context x Γ

theorem not_context_terms_to_not_in_context (x : ℕ) (Γ : context) : x ∉ context_terms Γ → ¬in_context x Γ

theorem in_context_append_neg (x : ℕ) (Γ Δ : context) : ¬in_context x (Γ ++ Δ) → ¬in_context x Γ ∧ ¬in_context x Δ

theorem in_context_append_neg' (x : ℕ) (Γ Δ : context) : ¬in_context x Γ ∧ ¬in_context x Δ → ¬in_context x (Γ ++ Δ)

inductive valid_ctx : context → Prop

• valid_nil : valid_ctx []
• valid_cons (Γ : context) (x : ℕ) (T : Typ) : valid_ctx Γ → ¬in_context x Γ → valid_ctx ((x, T) :: Γ)

theorem valid_push (Γ : context) (x : ℕ) (T : Typ) : valid_ctx Γ → ¬in_context x Γ → valid_ctx ([(x, T)] ++ Γ)

theorem valid_remove_mid (Γ Δ Ψ : context) : valid_ctx (Ψ ++ Δ ++ Γ) → valid_ctx (Ψ ++ Γ)

theorem valid_remove_mid_cons (x : ℕ) (T : Typ) (Γ Δ : context) : valid_ctx (Δ ++ (x, T) :: Γ) → valid_ctx (Δ ++ Γ)

theorem valid_remove_cons (x : ℕ) (T : Typ) (Γ : context) : valid_ctx ((x, T) :: Γ) → valid_ctx Γ

def get (x : ℕ) : context → Option Typ

Equations

• _root_.get x [] = none
• _root_.get x ((x_2, snd) :: Γ') = if x = x_2 then some snd else _root_.get x Γ'

def binds (x : ℕ) (T : Typ) (Γ : context) : Prop

Equations

• binds x T Γ = (_root_.get x Γ = some T)

theorem binds_singleton (x : ℕ) (T : Typ) : binds x T [(x, T)]

theorem binds_singleton_tail (x : ℕ) (T : Typ) (Γ : context) : binds x T ([(x, T)] ++ Γ)

theorem binds_tail (x : ℕ) (T : Typ) (Γ Δ : context) : binds x T Γ → ¬in_context x Δ → binds x T (Δ ++ Γ)

theorem binds_head (x : ℕ) (T : Typ) (Γ Δ : context) : binds x T Γ → binds x T (Γ ++ Δ)

theorem binds_concat_inv' (x : ℕ) (T : Typ) (Γ Δ : context) : binds x T (Γ ++ Δ) → in_context x Γ ∨ ¬binds x T Δ → binds x T Γ

theorem binds_concat_inv (x : ℕ) (T : Typ) (Γ Δ : context) : binds x T (Γ ++ Δ) → ¬in_context x Γ ∧ binds x T Δ ∨ binds x T Γ

theorem binds_singleton_inv (x y : ℕ) (X Y : Typ) : binds x X [(y, Y)] → x = y ∧ X = Y

theorem binds_mid (x : ℕ) (T : Typ) (Δ Γ : context) : valid_ctx (Γ ++ [(x, T)] ++ Δ) → binds x T (Γ ++ [(x, T)] ++ Δ)

theorem binds_mid_eq (x : ℕ) (T S : Typ) (Γ Δ : context) : binds x T (Δ ++ [(x, S)] ++ Γ) → valid_ctx (Δ ++ [(x, S)] ++ Γ) → T = S

theorem binds_mid_eq_cons (x : ℕ) (T S : Typ) (Γ Δ : context) : binds x T (Δ ++ (x, S) :: Γ) → valid_ctx (Δ ++ (x, S) :: Γ) → T = S

theorem binds_in_context (x : ℕ) (T : Typ) (Γ : context) : binds x T Γ → in_context x Γ

theorem binds_fresh (x : ℕ) (T : Typ) (Γ : context) : ¬in_context x Γ → ¬binds x T Γ

theorem binds_concat_ok (x : ℕ) (T : Typ) (Γ Δ : context) : binds x T Γ → valid_ctx (Δ ++ Γ) → binds x T (Δ ++ Γ)

theorem binds_weaken (x : ℕ) (T : Typ) (Γ Δ Ψ : context) : binds x T (Ψ ++ Γ) → valid_ctx (Ψ ++ Δ ++ Γ) → binds x T (Ψ ++ Δ ++ Γ)

theorem binds_weaken_at_head (x : ℕ) (T : Typ) (Γ Δ : context) : binds x T Δ → valid_ctx (Γ ++ Δ) → binds x T (Γ ++ Δ)

theorem binds_remove_mid (x y : ℕ) (T S : Typ) (Γ Δ : context) : binds x T (Γ ++ ([(y, S)] ++ Δ)) → x ≠ y → binds x T (Γ ++ Δ)

theorem binds_remove_mid_cons (x y : ℕ) (T S : Typ) (Γ Δ : context) : binds x T (Δ ++ (y, S) :: Γ) → x ≠ y → binds x T (Δ ++ Γ)