Support mixed induction/coinduction with Inf type

Update totality checker so that it checks for 'Delay LazyCodata' being
guarded by constructors/lambdas only, allowing mixed
inductive/coinductive definitions.
Change reduction rules for coinductive definitions

Allow reduction in types, but block any reduction immediately under a
Delay. This means coinductive proofs should now be possible, and
coinductive definitions should be runnable at the REPL even if the
produce an infinite stream.