At type level, how do I enforce possbility of pattern match?

Stream: lean4

[nrs]

inductive Term where
| var : String -> Term
| (other Terms)
prefix: max "!!" => Term.var

I'd like to make a function (t: Term) -> Term that enforces that t = !!s, i.e., that it must be able to pattern-match on !!s. How could I encode this on the type-level?

[nrs]

Argh, just realized this is the wrong channel. very sorry