Basic syntactic metatheory.

theorem EqTp.le_univMax {Γ : Ctx} {A B : Expr} {l : ℕ} : Γ ⊢[l] A ≡ B → l ≤ univMax

theorem EqTm.le_univMax {Γ : Ctx} {A t u : Expr} {l : ℕ} : Γ ⊢[l] t ≡ u : A → l ≤ univMax

theorem EqTp.wf_left {Γ : Ctx} {A B : Expr} {l : ℕ} : Γ ⊢[l] A ≡ B → Γ ⊢[l] A

theorem EqTp.wf_right {Γ : Ctx} {A B : Expr} {l : ℕ} : Γ ⊢[l] A ≡ B → Γ ⊢[l] B

theorem EqTm.wf_left {Γ : Ctx} {A t u : Expr} {l : ℕ} : Γ ⊢[l] t ≡ u : A → Γ ⊢[l] t : A

theorem EqTm.wf_right {Γ : Ctx} {A t u : Expr} {l : ℕ} : Γ ⊢[l] t ≡ u : A → Γ ⊢[l] u : A

theorem EqTm.wf_tp {Γ : Ctx} {A t u : Expr} {l : ℕ} : Γ ⊢[l] t ≡ u : A → Γ ⊢[l] A

theorem Lookup.wf_tp {Γ : Ctx} {i : ℕ} {A : Expr} {l : ℕ} : Lookup Γ i A l → Γ ⊢[l] A

theorem Lookup.wf_bvar {Γ : Ctx} {i : ℕ} {A : Expr} {l : ℕ} : Lookup Γ i A l → Γ ⊢[l] Expr.bvar i : A