jcmckeown

(** Approximating decidable equality for the type nCk.
 
As with GlobSet and DeltaSet, we implement locally the needed homotopy theory (which is trivial);
 `Require Import Homotopy` will do as well, modulo some notation, some names. I'd also bet some
 disappointment that the rhyming staves at the end of `nCk_uniq` are encapsulated in some named
 Lemma in `Homotopy`. Since the path arguments to `trans` in the concluding Lemma are cases of
 `@path nat`, which is a proposition in the sense of Voevodsky, it should be straight-forward (if
 tedious) to produce decidable equality in `nCk` by using those in `(list bool)` and `nat`.
*)