Theorem: Lean4Lean.liftVar_comp (Lean4Lean/Theory/VExpr.lean)

State before:
l₁ l₂ : Lift
n : Nat
⊢ Lift.liftVar (Lift.comp l₁ l₂) n = Lift.liftVar l₂ (Lift.liftVar l₁ n)
Tactic:
induction l₂ generalizing l₁ n <;> [skip; skip; cases l₁ <;> [skip; skip; cases n]] <;> simp [*]
State after:
no goals