Explain inspect idiom

[rodrigogribeiro]

Agda's inspect idiom is the way we simulate a behaviour similar to Coq's remember tactic --- introduce a equality on a expression that we want to pattern match on it, "remembering" its shape before the pattern match.

An explanation of the types used is highly necessary.