Theorem: Lean4Lean.Lift.consN_comp (Lean4Lean/Theory/VExpr.lean)

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