aesop ignores @[eliminator]

[kim-em]

It would be lovely if aesops cases rules used the @[eliminator] attributes, like induction and cases do:

import Aesop

structure Opposite (α : Type _) :=
  /-- The canonical map `αᵒᵖ → α`. -/
  unop : α

namespace Opposite

def op (x : α) : Opposite α := ⟨x⟩

@[eliminator]
protected def rec' {F : Opposite α → Sort v} (h : ∀ X, F (op X)) : ∀ X, F X := fun X => h (unop X)

example (x : Opposite α) : x = x := by
  induction x with
  | _ X => 
    guard_target = op X = op X
    rfl

attribute [aesop safe cases] Opposite

theorem bar (x y : Opposite α) : x = y := by
  aesop (options := { warnOnNonterminal := false })
  -- Oops, used Opposite.casesOn, not Opposite.rec
  sorry

#print bar 

[JLimperg]

This would indeed be nice. Problem: the MetaM cases tactic, which cases rules use, doesn't support custom eliminators (and it would be nontrivial to add this support). Possible solution: use the ElabM cases tactic. This would have to be lowered to MetaM, but maybe that's not an issue in practice. It might also resolve some issues with the tactic script generation functionality, where the discrepancy between MetaM cases and ElabM cases can lead to bugs.