Theorem: Lean4Lean.VExpr.Skips.of_instL (Lean4Lean/Theory/VExpr.lean)

State before:
ls : List VLevel
e : VExpr
n k : Nat
self : Skips (instL ls e) n k
⊢ Skips e n k
Tactic:
rw [skips_iff] at self ⊢
State after:
ls : List VLevel
e : VExpr
n k : Nat
self : Skips' n (instL ls e) k
⊢ Skips' n e k

State before:
ls : List VLevel
e : VExpr
n k : Nat
self : Skips' n (instL ls e) k
⊢ Skips' n e k
Tactic:
induction e generalizing k <;> simp_all [Skips']
State after:
no goals