Theorem: Lean4Lean.InScope.natLitToConstructor (Lean4Lean/Verify/Typing/Lemmas.lean)

State before:
P : FVarId → Prop
n k : Nat
⊢ InScope P (Expr.natLitToConstructor n) k
Tactic:
cases n <;> simp [InScope]
State after:
no goals