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

State before:
l : Lift
k : Nat
⊢ consN (skip l) k = comp (consN l k) (consN (skipN 1) k)
Tactic:
rw [← consN_comp]
State after:
l : Lift
k : Nat
⊢ consN (skip l) k = consN (comp l (skipN 1)) k

State before:
l : Lift
k : Nat
⊢ consN (skip l) k = consN (comp l (skipN 1)) k
Tactic:
rfl
State after:
no goals