{motive : Lean.Elab.Tactic.GuardExpr.MatchKind → Sort u} →
  (t : Lean.Elab.Tactic.GuardExpr.MatchKind) →
    motive Lean.Elab.Tactic.GuardExpr.MatchKind.syntactic →
      ((red : Lean.Meta.TransparencyMode) → motive (Lean.Elab.Tactic.GuardExpr.MatchKind.defEq red)) →
        motive Lean.Elab.Tactic.GuardExpr.MatchKind.alphaEq → motive t