compatibility with Dedukti 2.6

See merge request cauderlier/dktactics!1

This is probably a bit more portable

update installation instructions

This is the smallest proof produced by prover9 that uses both rules of resolution.

did not reduce

A dependent substitution is a substitution from formulae to formulae
that can act depend on the topmost universally quantified variables of
the formula.  This is going to be useful for handling substitutions of
clauses.

This structure is intended to be used for resolution and
paramodulation tactics. Having both clauses under the same quantifiers
allows to perform shallow unification.