added typing_empty_typing_te, extend_swap, stuck in closed substitution
typing_empty_te: if some expression types to t in a empty envrionment,
                 it types to to anywhere.
extend_swap: extending environments commutes for non-identical variables
closed_substitution : if a variable is replaced by a term of same type,
                      type of expressions never changes.