∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {inst : Std.LawfulIdentity ctx.op (Lean.Grind.AC.Var.denote ctx 0)}
  (s : Lean.Grind.AC.Seq), Lean.Grind.AC.Seq.denote ctx s.erase0 = Lean.Grind.AC.Seq.denote ctx s