∀ (r₁ c r₂ lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs : Lean.Grind.AC.Seq),
  Lean.Grind.AC.superpose_ac_cert r₁ c r₂ lhs₁ rhs₁ lhs₂ rhs₂ lhs rhs =
    (((lhs₁.beq' (c.union_k r₁)).and' (lhs₂.beq' (c.union_k r₂))).and' (lhs.beq' (r₂.union_k rhs₁))).and'
      (rhs.beq' (r₁.union_k rhs₂))