Library prosa.util.bigcat

Require Export prosa.util.tactics prosa.util.notation.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

(* Lemmas about the big concatenation operator. *)
Section BigCatLemmas.

  Lemma mem_bigcat_nat:
    ∀ (T: eqType) x m n j (f: _ → list T),
      m ≤ j < n →
      x \in (f j) →
      x \in \cat_(m ≤ i < n) (f i).

  Lemma mem_bigcat_nat_exists :
    ∀ (T: eqType) x m n (f: nat → list T),
      x \in \cat_(m ≤ i < n) (f i) →
      ∃ i, x \in (f i) ∧
                m ≤ i < n.

  Lemma bigcat_nat_uniq :
    ∀ (T: eqType) n1 n2 (F: nat → list T),
      (∀ i, uniq (F i)) →
      (∀ x i1 i2,
         x \in (F i1) → x \in (F i2) → i1 = i2) →
      uniq (\cat_(n1 ≤ i < n2) (F i)).

End BigCatLemmas.