Theorem: Lean4Lean.VExpr.unliftN_succ' (Lean4Lean/Theory/VExpr.lean)

State before:
e : VExpr
n k : Nat
⊢ unliftN e (n + 1) k = inst (unliftN e n k) default k
Tactic:
rw [unliftN_add]
State after:
e : VExpr
n k : Nat
⊢ unliftN (unliftN e n k) 1 k = inst (unliftN e n k) default k

State before:
e : VExpr
n k : Nat
⊢ unliftN (unliftN e n k) 1 k = inst (unliftN e n k) default k
Tactic:
rfl
State after:
no goals