Instantiation of Laws
In order to make proving a pure point-and-click activity, instantiation of laws has to be done automatically. Fortunately, given a focus expression and one side of a law, it is a purely automatic process to match those two expressions and instantiate the ∀-quantified variables in the law. This is what unification does! In instantiating quantified variables the law of generalisation is implicitly applied. In formal on-paper proofs this application of the law is never mentioned and taking for granted (especially since the laws are often not even written in quantified form).
Instantiation of Variables in the Focus
To use the Specialisation and The laws Unification is also used when we want to apply