Revert "Revert "remove "induction constant" and "dependent type"""

This reverts commit a5c5983bc4ac0a69f2e2756544e624db9a097551.