Add documentation on variable remove

[lbinria]

Description

Add documentation on variable remove.

• No variable remove in user defined function, all variables are considered as used.
• No variable remove when using in instruction in seq part, if r := something, r is considered as used even if not used in guard / invariant due to strict evaluation.