{P : Sort u} →
  {i : Lean.IR.CtorInfo} →
    {ys : Array Lean.IR.Arg} →
      {i' : Lean.IR.CtorInfo} →
        {ys' : Array Lean.IR.Arg} → Lean.IR.Expr.ctor i ys = Lean.IR.Expr.ctor i' ys' → (i = i' → ys = ys' → P) → P