Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2005-03-31 20:59:24 -0800 (Thu, 31 Mar 2005)
Revision: 7077
Log message:
Typing rule for dependent elimination for mutually inductive definitions.
It compiles but it is not sound yet.