Path of signature containing unificaton rules symbols.

Ghost signature holding the symbols used in unification rules.

• All signatures depend on it (dependency set in Sig_state.create_sign).
• All signatures open it (opened in Sig_state.of_sign).
• It is automatically loaded.

Symbol "≡".

Symbol ";".

unpack eqs transforms a term of the form cons (equiv t u) (cons (equiv v w) ...) into a list [(t,u); (v,w); ...].

mem s is true iff s belongs to sign.