Theorem: Lean4Lean.VEnv.CtxStrong.strong' (Lean4Lean/Theory/Typing/Strong.lean)

State before:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
hΓ : OnCtx Γ (IsType env U)
⊢ CtxStrong env U Γ
Tactic:
induction Γ with
| nil => trivial
| cons _ _ ih => let ⟨hΓ, _, hA⟩ := hΓ; exact ⟨ih hΓ, _, hA.strong' henv envIH (ih hΓ)⟩
State after:
no goals

State before:
case nil
env : VEnv
U : Nat
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
hΓ : OnCtx [] (IsType env U)
⊢ CtxStrong env U []
Tactic:
trivial
State after:
no goals

State before:
case cons
env : VEnv
U : Nat
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
head✝ : VExpr
tail✝ : List VExpr
ih : OnCtx tail✝ (IsType env U) → CtxStrong env U tail✝
hΓ : OnCtx (head✝ :: tail✝) (IsType env U)
⊢ CtxStrong env U (head✝ :: tail✝)
Tactic:
let ⟨hΓ, _, hA⟩ := hΓ
State after:
case cons
env : VEnv
U : Nat
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
head✝ : VExpr
tail✝ : List VExpr
ih : OnCtx tail✝ (IsType env U) → CtxStrong env U tail✝
hΓ✝ : OnCtx (head✝ :: tail✝) (IsType env U)
hΓ : OnCtx tail✝ (IsType env U)
w✝ : VLevel
hA : HasType env U tail✝ head✝ (sort w✝)
⊢ CtxStrong env U (head✝ :: tail✝)

State before:
case cons
env : VEnv
U : Nat
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
head✝ : VExpr
tail✝ : List VExpr
ih : OnCtx tail✝ (IsType env U) → CtxStrong env U tail✝
hΓ✝ : OnCtx (head✝ :: tail✝) (IsType env U)
hΓ : OnCtx tail✝ (IsType env U)
w✝ : VLevel
hA : HasType env U tail✝ head✝ (sort w✝)
⊢ CtxStrong env U (head✝ :: tail✝)
Tactic:
exact ⟨ih hΓ, _, hA.strong' henv envIH (ih hΓ)⟩
State after:
no goals