(motive :
    MProd (Array Lean.Compiler.LCNF.Arg) (MProd (Array Lean.Compiler.LCNF.Param) Lean.Compiler.LCNF.FVarSubst) →
      Sort u_1) →
  (r : MProd (Array Lean.Compiler.LCNF.Arg) (MProd (Array Lean.Compiler.LCNF.Param) Lean.Compiler.LCNF.FVarSubst)) →
    ((jpArgs : Array Lean.Compiler.LCNF.Arg) →
        (jpParams : Array Lean.Compiler.LCNF.Param) →
          (subst : Lean.Compiler.LCNF.FVarSubst) → motive ⟨jpArgs, jpParams, subst⟩) →
      motive r