Theorem: Lean4Lean.VLCtx.LiftN.wf (Lean4Lean/Verify/Typing/Lemmas.lean)

State before:
env : VEnv
henv : Ordered env
Δ Δ' : VLCtx
dk n k U : Nat
W : LiftN Δ Δ' dk n k
hΔ' : WF env U Δ'
⊢ WF env U Δ
Tactic:
induction W with
| refl => exact hΔ'
| skip_fvar _ _ _ ih => exact ih hΔ'.1
| cons_bvar _ W ih =>
  let ⟨hΔ', _, h2⟩ := hΔ'
  exact ⟨ih hΔ', nofun, (VLocalDecl.weakN_iff henv hΔ'.toCtx W.toCtx).1 h2⟩
State after:
no goals

State before:
case refl
env : VEnv
henv : Ordered env
Δ Δ' : VLCtx
dk n k U : Nat
Δ✝ : VLCtx
hΔ' : WF env U Δ✝
⊢ WF env U Δ✝
Tactic:
exact hΔ'
State after:
no goals

State before:
case skip_fvar
env : VEnv
henv : Ordered env
Δ Δ' : VLCtx
dk n k U : Nat
Δ✝ Δ'✝ : VLCtx
n✝ : Nat
fv✝ : FVarId
d✝ : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ 0 n✝ 0
ih : WF env U Δ'✝ → WF env U Δ✝
hΔ' : WF env U ((some fv✝, d✝) :: Δ'✝)
⊢ WF env U Δ✝
Tactic:
exact ih hΔ'.1
State after:
no goals

State before:
case cons_bvar
env : VEnv
henv : Ordered env
Δ Δ' : VLCtx
dk n k U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d✝ : VLocalDecl
W : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih : WF env U Δ'✝ → WF env U Δ✝
hΔ' : WF env U ((none, VLocalDecl.liftN d✝ n✝ k✝) :: Δ'✝)
⊢ WF env U ((none, d✝) :: Δ✝)
Tactic:
let ⟨hΔ', _, h2⟩ := hΔ'
State after:
case cons_bvar
env : VEnv
henv : Ordered env
Δ Δ' : VLCtx
dk n k U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d✝ : VLocalDecl
W : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih : WF env U Δ'✝ → WF env U Δ✝
hΔ'✝ : WF env U ((none, VLocalDecl.liftN d✝ n✝ k✝) :: Δ'✝)
hΔ' : WF env U Δ'✝
left✝ : ∀ (fv : FVarId), none = some fv → ¬fv ∈ fvars Δ'✝
h2 : VLocalDecl.WF env U (VLCtx.toCtx Δ'✝) (VLocalDecl.liftN d✝ n✝ k✝)
⊢ WF env U ((none, d✝) :: Δ✝)

State before:
case cons_bvar
env : VEnv
henv : Ordered env
Δ Δ' : VLCtx
dk n k U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d✝ : VLocalDecl
W : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih : WF env U Δ'✝ → WF env U Δ✝
hΔ'✝ : WF env U ((none, VLocalDecl.liftN d✝ n✝ k✝) :: Δ'✝)
hΔ' : WF env U Δ'✝
left✝ : ∀ (fv : FVarId), none = some fv → ¬fv ∈ fvars Δ'✝
h2 : VLocalDecl.WF env U (VLCtx.toCtx Δ'✝) (VLocalDecl.liftN d✝ n✝ k✝)
⊢ WF env U ((none, d✝) :: Δ✝)
Tactic:
exact ⟨ih hΔ', nofun, (VLocalDecl.weakN_iff henv hΔ'.toCtx W.toCtx).1 h2⟩
State after:
no goals