Theorem: Lean4Lean.VExpr.lift'_comp (Lean4Lean/Theory/VExpr.lean)

State before:
l₁ l₂ : Lift
e : VExpr
⊢ lift' (lift' e l₁) l₂ = lift' e (Lift.comp l₁ l₂)
Tactic:
induction e generalizing l₁ l₂ <;> simp [liftVar_comp, *]
State after:
no goals