I was referring to https://link.springer.com/chapter/10.1007/3-540-45413-6_16; induction is not derivable in pure CoC. I suppose yes technically you could base a dependently-typed language on it if you didn't mind not supporting induction, but I can't imagine many people wanting to use it, as it would be quite limited compared to one supporting inductive proofs. Or at least when people think of "dependently typed programming language", they're usually thinking of something at least as expressive as CIC.