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

State before:
P : FVarId → Prop
s : String
k : Nat
⊢ InScope P (Expr.strLitToConstructor s) k
Tactic:
simp [InScope, String.foldr_eq]
State after:
P : FVarId → Prop
s : String
k : Nat
⊢ InScope P
    (List.foldr
      (fun c e =>
        Expr.app
          (Expr.app (Expr.app (Expr.const `List.cons [Level.zero]) (Expr.const `Char []))
            (Expr.app (Expr.const `Char.ofNat []) (Expr.lit (Literal.natVal (Char.toNat c)))))
          e)
      (Expr.app (Expr.const `List.nil [Level.zero]) (Expr.const `Char [])) s.data)
    k

State before:
P : FVarId → Prop
s : String
k : Nat
⊢ InScope P
    (List.foldr
      (fun c e =>
        Expr.app
          (Expr.app (Expr.app (Expr.const `List.cons [Level.zero]) (Expr.const `Char []))
            (Expr.app (Expr.const `Char.ofNat []) (Expr.lit (Literal.natVal (Char.toNat c)))))
          e)
      (Expr.app (Expr.const `List.nil [Level.zero]) (Expr.const `Char [])) s.data)
    k
Tactic:
induction s.data <;> simp [*, InScope]
State after:
no goals