Depending on dktactics makes writing the interoperability layer hard
because most types in dktactics are not definable.

Moreover, this removes dependency on Dedukti v2.6 (featuring injective
symbols). When the transfer tactic will be called, it will not know
about the rule [a,b] term (arr a b) --> term a -> term b.