{α : Type u} →
  {P : Sort u_1} →
    {a : ℕ} →
      {a_1 a_2 : Lean.RArray α} →
        {a' : ℕ} →
          {a'_1 a'_2 : Lean.RArray α} →
            Lean.RArray.branch a a_1 a_2 = Lean.RArray.branch a' a'_1 a'_2 → (a = a' → a_1 ≍ a'_1 → a_2 ≍ a'_2 → P) → P