chore: fix for lean4#5542

In lean4#5542 we will be deprecating `structure ... :=` in favor of
`structure ... where`.

Qq/Typ.lean

@@ -37,15 +37,15 @@ protected abbrev Quoted.ty (t : Quoted α) : Expr := α
 
 You should usually write this using the notation `$lhs =Q $rhs`.
 -/
-structure QuotedDefEq {α : Quoted (.sort u)} (lhs rhs : Quoted α) : Prop :=
+structure QuotedDefEq {α : Quoted (.sort u)} (lhs rhs : Quoted α) : Prop where
   unsafeIntro ::
 
 /--
 `QuotedLevelDefEq u v` says that the levels `u` and `v` are definitionally equal.
 
 You should usually write this using the notation `$u =QL $v`.
 -/
-structure QuotedLevelDefEq (u v : Level) : Prop :=
+structure QuotedLevelDefEq (u v : Level) : Prop where
   unsafeIntro ::
 
 open Meta in