(motive :
    Option
        (Lean.Compiler.LCNF.Param Lean.Compiler.LCNF.Purity.impure ×
          Subarray (Lean.Compiler.LCNF.Param Lean.Compiler.LCNF.Purity.impure)) →
      Sort u_1) →
  (x :
      Option
        (Lean.Compiler.LCNF.Param Lean.Compiler.LCNF.Purity.impure ×
          Subarray (Lean.Compiler.LCNF.Param Lean.Compiler.LCNF.Purity.impure))) →
    (Unit → motive none) →
      ((newParam : Lean.Compiler.LCNF.Param Lean.Compiler.LCNF.Purity.impure) →
          (s' : Subarray (Lean.Compiler.LCNF.Param Lean.Compiler.LCNF.Purity.impure)) → motive (some (newParam, s'))) →
        motive x