conclude term

The current conclusion must be an equality t1 = tk

It starts an equality chain on the conclusion. It allows the user to apply the tactic = to continue the chain.

None.