Translating Lean to Dedukti