{P : Sort u} →
  {ref : Lean.Syntax} →
    {jpName : Lean.Name} →
      {args : Array Lean.Syntax} →
        {ref' : Lean.Syntax} →
          {jpName' : Lean.Name} →
            {args' : Array Lean.Syntax} →
              Lean.Elab.Term.Do.Code.jmp ref jpName args = Lean.Elab.Term.Do.Code.jmp ref' jpName' args' →
                (ref = ref' → jpName = jpName' → args = args' → P) → P