def Lean.LocalContext.getRoundtrippingUserName? (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) : Option Lean.Name

Given an FVarId, this function returns the corresponding user name, but only if the name can be used to recover the original FVarId.