Theorem: Lean4Lean.Ctx.Lift'.depth_zero (Lean4Lean/Theory/Typing/Lemmas.lean)

State before:
l✝ : Lift
Γ Γ' : List VExpr
l : Lift
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
H : Lift' l Γ✝ Γ'✝
h : Lift.depth (Lift.cons l) = 0
⊢ A✝ :: Γ✝ = lift' A✝ l :: Γ'✝
Tactic:
rw [VExpr.lift'_depth_zero (l := l) h, H.depth_zero (l := l) h]
State after:
no goals