{pu : Lean.Compiler.LCNF.Purity} →
  (motive : Lean.Compiler.LCNF.Decl pu → Lean.Compiler.LCNF.Decl pu → Sort u_1) →
    (x x_1 : Lean.Compiler.LCNF.Decl pu) →
      ((a : Lean.Compiler.LCNF.Signature pu) →
          (a_1 : Lean.Compiler.LCNF.DeclValue pu) →
            (a_2 : Bool) →
              (a_3 : Option Lean.Compiler.InlineAttributeKind) →
                (b : Lean.Compiler.LCNF.Signature pu) →
                  (b_1 : Lean.Compiler.LCNF.DeclValue pu) →
                    (b_2 : Bool) →
                      (b_3 : Option Lean.Compiler.InlineAttributeKind) →
                        motive { toSignature := a, value := a_1, recursive := a_2, inlineAttr? := a_3 }
                          { toSignature := b, value := b_1, recursive := b_2, inlineAttr? := b_3 }) →
        ((x x_2 : Lean.Compiler.LCNF.Decl pu) → motive x x_2) → motive x x_1