∀ {lhs : Bool} {s₁ s₂ : Lean.Grind.AC.Seq} {c₁ : Lean.Meta.Grind.AC.EqCnstr} {c₂ : Lean.Meta.Grind.AC.DiseqCnstr}
  {lhs_1 : Bool} {s₁_1 s₂_1 : Lean.Grind.AC.Seq} {c₁_1 : Lean.Meta.Grind.AC.EqCnstr}
  {c₂_1 : Lean.Meta.Grind.AC.DiseqCnstr},
  Lean.Meta.Grind.AC.DiseqCnstrProof.simp_middle lhs s₁ s₂ c₁ c₂ =
      Lean.Meta.Grind.AC.DiseqCnstrProof.simp_middle lhs_1 s₁_1 s₂_1 c₁_1 c₂_1 →
    lhs = lhs_1 ∧ s₁ = s₁_1 ∧ s₂ = s₂_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1