§ Lean Naming Convention for Contexts

• LocalContext contains LocalDecls, and is owned by a Metavar.
• MetavarContext contains Metavars, and is owned by a MetaM.
• TacticM contains the list of goal [goal : MVarId].