Added "strong induction" (`lt` is a well-founded relation) for some reason.
Not sure it's needed, but one never can tell.

Now defined: all the facets of a cell  (in terms of the `nCkList`
 holding them); the derived adjacency relation of closed cells; starting
on closure, the reflection of a closed cell as the cell of its faces.

The sticky point is to show that two things are equal :
~~~~~
_____ :
fun_list (skel k C) (nCkCompose (l; (cx, y)) x) =
fun_list (skel k (fun_list (depS_lS' (skel (S k) C) (l; y)) cx)) x
~~~~~
which is just to say that the facet at a binomial composite is the iterated
facet at the separate binomials.


Signed-off-by: jcmckeown <jesse@sockwright>