Dedukti Level Implementation