theory Context_Extra imports First_Order_Terms.Subterm_and_Context begin no_notation subst_compose (infixl "∘⇩s" 75) no_notation subst_apply_term (infixl "⋅" 67) end