Support for inductive-inductive types

Add constructors to context immediately after elaborating, rather than
adding the whole data type at once, so that later constructors can use
them. Fixes #1757.