pattern matching over Ast.Case simplified:

- it is not possible to match the `in intype` foo part
- it is not possible to match the outtype
eta expansion still done on Ast (hard to do it in Cic. The abstracted variable
does not have a type :-( thus you may have to double your notations. Name for fresh variables changed to \etaX instead of freshX (much shorter in terms of screen pixels)