Does anyone have an example of a LetRecToLift?

Stream: metaprogramming / tactics

[nrs]

Trying to work my way through the elaboration of let rec expressions. I'm wondering, does anyone have an example of a term that will produce, in TermElabM, a value for a LetRecToLift structure, and the value itself?