Add how dependent pattern matching works for anonymous `have` expressions and `show` expressions (the inductive definition is called `this`).
Add how dependent pattern matching works for anonymous
haveexpressions andshowexpressions (the inductive definition is calledthis).