stuck in closed substitution, added identical_extend_identical and exchangeable_context.
identical_extend_identical: if two typing environments are similar at all places and receive the same extension,
  the extended environments are similar in all places
exchangeable_context: typing does not change if environment is exchanged for environment
  that is the same for all variables