{α : Sort u} →
  {op : α → α → α} →
    {motive : Lean.Data.AC.Variable op → Sort u_1} →
      (t : Lean.Data.AC.Variable op) →
        ((value : α) →
            (neutral : Option (PLift (Std.LawfulIdentity op value))) → motive { value := value, neutral := neutral }) →
          motive t