{motive : Lean.Compiler.LCNF.Simp.CtorInfo → Sort u} →
  (t : Lean.Compiler.LCNF.Simp.CtorInfo) →
    ((val : Lean.ConstructorVal) →
        (args : Array (Lean.Compiler.LCNF.Arg Lean.Compiler.LCNF.Purity.pure)) →
          motive (Lean.Compiler.LCNF.Simp.CtorInfo.ctor val args)) →
      ((n : ℕ) → motive (Lean.Compiler.LCNF.Simp.CtorInfo.natVal n)) → motive t