Type Alias Substitution 

pub type Substitution = HashMap<String, ProofTerm>;

A substitution mapping variable names to terms.

Substitutions are the output of unification. Applying a substitution to both sides of a unification problem yields identical terms.

Example

After unifying Mortal(x) with Mortal(Socrates):

{ "x" ↦ Constant("Socrates") }

Operations

• unify_terms - Creates substitutions from term unification
• apply_subst_to_term - Applies substitution to a term
• compose_substitutions - Combines two substitutions

Aliased Type

pub struct Substitution { /* private fields */ }