0art0

import Lean
import Lean.Elab
import Lean.Elab.Tactic
import Lean.Meta
open Lean Expr Elab Meta Tactic

set_option pp.proofs true
set_option pp.proofs.withType true

/-