Preliminaries

QuasiTerms_Swap_Fresh

QuasiTerms_PickFresh_Alpha

QuasiTerms_Environments_Substitution

Pick

Equiv_Relation2

Transition_QuasiTerms_Terms

Terms

Well_Sorted_Terms

Iteration

Semantic_Domains

Recursion