judging for the same constructor

Stream: Is there code for X?

[Yingte Xu]

I am trying to judge whether two instances are constructed in the same way. The following code works, but is there a better way?

inductive AV : Type where
  | x
  | y

def AV_eq (av1 : AV) (av2 : AV) : Bool :=
  match av1 with
  | AV.x => match av2 with
    | AV.x => True
    | _ => False
  | AV.y => match av2 with
    | AV.y => True
    | _ => False