Adding some theory for `rem` and generalizing `subset_maskP`

- Added helper lemmas about `rem`: `rem_cons` (to control unfolding),
  `remE`, `count_rem`, `count_mem_rem`, and `subseq_mem`.
  (New lemma `drop_index` briges the gap between `cat_take_drop` and `remE`).
- `subset_maskP`, which was not released yet is generalized with
  hypothesis `(forall x, count_mem x s1 <= count_mem x s2)`, instead of
  `uniq s1` and `{subset s1 <= s2}`, the previous behaviour can be
  restored with helper lemma `leq_uniq_count`
- Its trivial consequence `subset_subseqP` has been added too.

0 files changed, 0 insertions, 0 deletions