{P : Sort u} →
  {f : Lean.IR.FunId} →
    {xs : Array Lean.IR.Param} →
      {type : Lean.IR.IRType} →
        {body : Lean.IR.FnBody} →
          {info : Lean.IR.DeclInfo} →
            {f' : Lean.IR.FunId} →
              {xs' : Array Lean.IR.Param} →
                {type' : Lean.IR.IRType} →
                  {body' : Lean.IR.FnBody} →
                    {info' : Lean.IR.DeclInfo} →
                      Lean.IR.Decl.fdecl f xs type body info = Lean.IR.Decl.fdecl f' xs' type' body' info' →
                        (f = f' → xs = xs' → type = type' → body = body' → info = info' → P) → P