Inductive definitions package almost completed
Inductive definitions package almost completed

NOTES:
1. only tested on our running example
2. it lacks the elimination principle only
3. it automatically derives:
   a) the functor predicate
   b) the proof that it is monotone
   c) the predicate as a fixpoint
   d) the technical introduction theorem
   e) for each constructor, the ad-hoc introduction theorem

LPCIC/elpi