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

State before:
env : VEnv
henv : Ordered env
Δ Δ' : VLCtx
dk n k : Nat
W : LiftN Δ Δ' dk n k
⊢ fvars Δ <:+ fvars Δ'
Tactic:
induction W with
| refl => exact List.suffix_refl _
| skip_fvar _ _ _ ih => exact ih.trans (List.suffix_cons ..)
| cons_bvar _ _ ih => exact ih
State after:
no goals

State before:
case refl
env : VEnv
henv : Ordered env
Δ Δ' : VLCtx
dk n k : Nat
Δ✝ : VLCtx
⊢ fvars Δ✝ <:+ fvars Δ✝
Tactic:
exact List.suffix_refl _
State after:
no goals

State before:
case skip_fvar
env : VEnv
henv : Ordered env
Δ Δ' : VLCtx
dk n k : Nat
Δ✝ Δ'✝ : VLCtx
n✝ : Nat
fv✝ : FVarId
d✝ : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ 0 n✝ 0
ih : fvars Δ✝ <:+ fvars Δ'✝
⊢ fvars Δ✝ <:+ fvars ((some fv✝, d✝) :: Δ'✝)
Tactic:
exact ih.trans (List.suffix_cons ..)
State after:
no goals

State before:
case cons_bvar
env : VEnv
henv : Ordered env
Δ Δ' : VLCtx
dk n k : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d✝ : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih : fvars Δ✝ <:+ fvars Δ'✝
⊢ fvars ((none, d✝) :: Δ✝) <:+ fvars ((none, VLocalDecl.liftN d✝ n✝ k✝) :: Δ'✝)
Tactic:
exact ih
State after:
no goals