work-in-progress well-ordered choice extensions:
  - forall combinators
  - order definitions
  - generalized skolem
  - classical contrapositives
  - new choice interface

So that we can keep working on the thing with Emacs and proof general.

This doesn't work apparently due to undesirable behaviour of unification.

WIP on CS-based implementation of finpred whose core only depends on Equality. Documentation to follow.

CS inference always fails in the argument of a match

We only have perm_eq (enum 'I_n) (iota 0 n) now,
this may break quite a few things.

This has required a major redesign of the finpred structures, since inference must now be triggered at the formula (bool) level, and derive the intended predicate using HO unification. There are some residual issues with coercions from finpred to pred, which will tend to cause undesireable expansion of predicate constants.

Moved away irrelevant code.
Moved support code to appropriate files, with documentation.
Declared mem_seq as a (non-uniform) coercion.

Moved away irrelevant code.
Moved support code to appropriate files, with documentation.
Declared mem_seq as a (non-uniform) coercion.