Commented definitions with holes.
Added elimination operator for `_<_` relation.
Wrote some stuff on collapsible families.