Changes by: Nataly Novak (nnovak at gc.cuny.edu)
Date: 2004-04-30 12:39:25 -0700 (Fri, 30 Apr 2004)
Revision: 5745
Log message:
For some reason CVS didn't commit cic-files in the previous commit
cic_lambda - dfun renamed to fun
cic_ind_type - bugfixes and some basic automation added
cic_list - nil_wf and cons_wf proved.
TODO:
1.Prove well-formedness of the inductive definition of List (list_wf, nil_wf, cons_wf proved)
2.Destructors & fixpoint for inductive definitions