{P : Sort u} →
  {lhs : Bool} →
    {s : Lean.Grind.AC.Seq} →
      {c₁ : Lean.Meta.Grind.AC.EqCnstr} →
        {c₂ : Lean.Meta.Grind.AC.DiseqCnstr} →
          {lhs' : Bool} →
            {s' : Lean.Grind.AC.Seq} →
              {c₁' : Lean.Meta.Grind.AC.EqCnstr} →
                {c₂' : Lean.Meta.Grind.AC.DiseqCnstr} →
                  Lean.Meta.Grind.AC.DiseqCnstrProof.simp_suffix lhs s c₁ c₂ =
                      Lean.Meta.Grind.AC.DiseqCnstrProof.simp_suffix lhs' s' c₁' c₂' →
                    (lhs = lhs' → s = s' → c₁ = c₁' → c₂ = c₂' → P) → P