Monoid_Action

Abstract_Substitution

Option_Extra

Substitution

Based_Substitution

Natural_Magma

Natural_Functor

Natural_Magma_Functor

Substitution_Lifting

Based_Substitution_Lifting

Substitution_First_Order_Term

Substitution_HOL_ex_Unification

Substitution_Lifting_Example