include in with variable in

Stream: general

[Christian Merten]

Consider the following MWE:

variable {M : Type} [Nonempty M]

/- many declarations where M implicit is good -/

variable (M) in
include M in
theorem foo : True := by
  apply Nonempty.elim ‹Nonempty M›
  intro m
  trivial

/- more declarations where M implicit is good -/

Is this the right way to enforce that M is usable in the body of foo and that M is an explicit variable? Or is there a shorter solution?

[Edward van de Meent]

if M is explicitly mentioned in the type of foo, you can drop the include, but otherwise yes.

[Christian Merten]

Thanks!