(motive : Lean.Compiler.LCNF.FixedParams.AbsValue → Lean.Compiler.LCNF.FixedParams.AbsValue → Sort u_1) →
  (x x_1 : Lean.Compiler.LCNF.FixedParams.AbsValue) →
    (Unit → motive Lean.Compiler.LCNF.FixedParams.AbsValue.top Lean.Compiler.LCNF.FixedParams.AbsValue.top) →
      (Unit → motive Lean.Compiler.LCNF.FixedParams.AbsValue.erased Lean.Compiler.LCNF.FixedParams.AbsValue.erased) →
        ((a b : ℕ) →
            motive (Lean.Compiler.LCNF.FixedParams.AbsValue.val a) (Lean.Compiler.LCNF.FixedParams.AbsValue.val b)) →
          ((x x_2 : Lean.Compiler.LCNF.FixedParams.AbsValue) → motive x x_2) → motive x x_1