Theorem: Lean4Lean.Ctx.LiftN.right (Lean4Lean/Theory/Typing/Lemmas.lean)

State before:
Γ : List VExpr
h : CtxClosed Γ
Γ' : List VExpr
x✝ : CtxClosed []
⊢ LiftN (List.length Γ') (List.length []) [] ([] ++ Γ')
Tactic:
simpa using LiftN.zero (Γ := []) Γ'
State after:
no goals

State before:
Γ✝ : List VExpr
h : CtxClosed Γ✝
Γ' : List VExpr
A : VExpr
Γ : List VExpr
h1 : OnCtx Γ fun Γ A => ClosedN A (List.length Γ)
h2 : (fun Γ A => ClosedN A (List.length Γ)) Γ A
⊢ LiftN (List.length Γ') (List.length (A :: Γ)) (A :: Γ) (A :: Γ ++ Γ')
Tactic:
simpa [h2.liftN_eq (Nat.le_refl _)] using LiftN.succ (LiftN.right h1 Γ') (A := A)
State after:
no goals