{pu : Lean.Compiler.LCNF.Purity} →
  {motive : Lean.Compiler.LCNF.Arg pu → Sort u} →
    (t : Lean.Compiler.LCNF.Arg pu) →
      motive Lean.Compiler.LCNF.Arg.erased →
        ((fvarId : Lean.FVarId) → motive (Lean.Compiler.LCNF.Arg.fvar fvarId)) →
          ((expr : Lean.Expr) →
              (h : pu = Lean.Compiler.LCNF.Purity.pure) → motive (Lean.Compiler.LCNF.Arg.type expr h)) →
            motive t