Elaborating Inductive Definitions and Course-of-Values Induction in Cedille