Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory