Denis Firsov, Aaron Stump: Generic derivation of induction for impredicative encodings in Cedille. CPP 2018: 215-227