Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-elpi.elpi ... done]
Require Export prosa.util.tactics prosa.util.notation.
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Require Export prosa.util.tactics prosa.util.list. (** In this section, we introduce lemmas about the concatenation operation performed over arbitrary sequences. *) Section BigCatNatLemmas. (** Consider any type [T] supporting equality comparisons... *) Variable T : eqType. (** ...and a function [f] that, given an index, yields a sequence. *) Variable f : nat -> seq T. (** In this section, we prove that the concatenation over sequences works as expected: no element is lost during the concatenation, and no new element is introduced. *) Section BigCatNatElements. (** First, we show that the concatenation comprises all the elements of each sequence; i.e. any element contained in one of the sequences will also be an element of the result of the concatenation. *)
T: eqType
f: nat -> seq T

forall (x : T) (m n j : nat), m <= j < n -> x \in f j -> x \in \cat_(m<=i<n)f i
T: eqType
f: nat -> seq T

forall (x : T) (m n j : nat), m <= j < n -> x \in f j -> x \in \cat_(m<=i<n)f i
T: eqType
f: nat -> seq T
x: T
m, n, j: nat
IN: x \in f j
LE: m <= j
LE0: j < n

x \in \cat_(m<=i<n)f i
T: eqType
f: nat -> seq T
x: T
m, n, j: nat
IN: x \in f j
LE: m <= j
LE0: j < n

x \in \cat_(m<=i<j)f i ++ \cat_(j<=i<n)f i
T: eqType
f: nat -> seq T
x: T
m, n, j: nat
IN: x \in f j
LE: m <= j
LE0: j < n

x \in \cat_(j<=i<n)f i
T: eqType
f: nat -> seq T
x: T
m, n, j: nat
IN: x \in f j
LE: m <= j
LE0: j < n.+1

x \in \cat_(j<=i<n.+1)f i
T: eqType
f: nat -> seq T
x: T
m, n, j: nat
IN: x \in f j
LE: m <= j
LE0: j < n.+1

x \in f j ++ \cat_(j<=i<n)f i.+1
by rewrite mem_cat; apply/orP; left. Qed. (** Conversely, we prove that any element belonging to a concatenation of sequences must come from one of the sequences. *)
T: eqType
f: nat -> seq T

forall (x : T) (m n : nat), x \in \cat_(m<=i<n)f i -> exists i : nat, x \in f i /\ m <= i < n
T: eqType
f: nat -> seq T

forall (x : T) (m n : nat), x \in \cat_(m<=i<n)f i -> exists i : nat, x \in f i /\ m <= i < n
T: eqType
f: nat -> seq T
x: T
m, n: nat
IN: x \in \cat_(m<=i<n)f i

exists i : nat, x \in f i /\ m <= i < n
T: eqType
f: nat -> seq T
x: T
m, n: nat
IHn: x \in \cat_(m<=i<n)f i -> exists i : nat, x \in f i /\ m <= i < n
IN: x \in \cat_(m<=i<n.+1)f i

exists i : nat, x \in f i /\ m <= i < n.+1
T: eqType
f: nat -> seq T
x: T
m, n: nat
IHn: x \in \cat_(m<=i<n)f i -> exists i : nat, x \in f i /\ m <= i < n
IN: x \in \cat_(m<=i<n.+1)f i
i: m <= n

exists i : nat, x \in f i /\ m <= i < n.+1
T: eqType
f: nat -> seq T
x: T
m, n: nat
IHn: x \in \cat_(m<=i<n)f i -> exists i : nat, x \in f i /\ m <= i < n
i: m <= n
IN: (x \in \cat_(m<=i<n)f i) || (x \in f n)

exists i : nat, x \in f i /\ m <= i < n.+1
T: eqType
f: nat -> seq T
x: T
m, n: nat
IHn: x \in \cat_(m<=i<n)f i -> exists i : nat, x \in f i /\ m <= i < n
i: m <= n
HEAD: x \in \cat_(m<=i<n)f i

exists i : nat, x \in f i /\ m <= i < n.+1
T: eqType
f: nat -> seq T
x: T
m, n: nat
IHn: x \in \cat_(m<=i<n)f i -> exists i : nat, x \in f i /\ m <= i < n
i: m <= n
TAIL: x \in f n
exists i : nat, x \in f i /\ m <= i < n.+1
T: eqType
f: nat -> seq T
x: T
m, n: nat
IHn: x \in \cat_(m<=i<n)f i -> exists i : nat, x \in f i /\ m <= i < n
i: m <= n
HEAD: x \in \cat_(m<=i<n)f i

exists i : nat, x \in f i /\ m <= i < n.+1
T: eqType
f: nat -> seq T
x: T
m, n: nat
IHn: x \in \cat_(m<=i<n)f i -> exists i : nat, x \in f i /\ m <= i < n
i: m <= n
HEAD: x \in \cat_(m<=i<n)f i
x0: nat
H: x \in f x0
H0: m <= x0
H1: x0 < n

x \in f x0 /\ m <= x0 < n.+1
T: eqType
f: nat -> seq T
x: T
m, n: nat
IHn: x \in \cat_(m<=i<n)f i -> exists i : nat, x \in f i /\ m <= i < n
i: m <= n
HEAD: x \in \cat_(m<=i<n)f i
x0: nat
H: x \in f x0
H0: m <= x0
H1: x0 < n

m <= x0 < n.+1
by apply/andP; split; last by apply ltnW.
T: eqType
f: nat -> seq T
x: T
m, n: nat
IHn: x \in \cat_(m<=i<n)f i -> exists i : nat, x \in f i /\ m <= i < n
i: m <= n
TAIL: x \in f n

exists i : nat, x \in f i /\ m <= i < n.+1
T: eqType
f: nat -> seq T
x: T
m, n: nat
IHn: x \in \cat_(m<=i<n)f i -> exists i : nat, x \in f i /\ m <= i < n
i: m <= n
TAIL: x \in f n

m <= n < n.+1
by apply/andP; split; last apply ltnSn. Qed. (** We also restate lemma [mem_bigcat_nat] in terms of ordinals. *)
T: eqType
f: nat -> seq T

forall (x : T) (n : nat) (j : 'I_n) (f : 'I_n -> seq T), j < n -> x \in f j -> x \in \cat_(i<n)f i
T: eqType
f: nat -> seq T

forall (x : T) (n : nat) (j : 'I_n) (f : 'I_n -> seq T), j < n -> x \in f j -> x \in \cat_(i<n)f i
T: eqType
f: nat -> seq T
x: T
n: nat
IHn: forall (j : 'I_n) (f : 'I_n -> seq T), j < n -> x \in f j -> x \in \cat_(i<n)f i
j: 'I_n.+1
f': 'I_n.+1 -> seq T
Hj: j < n.+1
Hx: x \in f' j

x \in \cat_(i<n.+1)f' i
T: eqType
f: nat -> seq T
x: T
n: nat
IHn: forall (j : 'I_n) (f : 'I_n -> seq T), j < n -> x \in f j -> x \in \cat_(i<n)f i
j: 'I_n.+1
f': 'I_n.+1 -> seq T
Hj: j < n.+1
Hx: x \in f' j

x \in \cat_(i<n)f' (widen_ord (m:=n.+1) (leqnSn n) i) \/ x \in f' ord_max
T: eqType
f: nat -> seq T
x: T
n: nat
IHn: forall (j : 'I_n) (f : 'I_n -> seq T), j < n -> x \in f j -> x \in \cat_(i<n)f i
j: 'I_n.+1
f': 'I_n.+1 -> seq T
Hx: x \in f' j
Hj: j = n

x \in \cat_(i<n)f' (widen_ord (m:=n.+1) (leqnSn n) i) \/ x \in f' ord_max
T: eqType
f: nat -> seq T
x: T
n: nat
IHn: forall (j : 'I_n) (f : 'I_n -> seq T), j < n -> x \in f j -> x \in \cat_(i<n)f i
j: 'I_n.+1
f': 'I_n.+1 -> seq T
Hx: x \in f' j
Hj: j < n
x \in \cat_(i<n)f' (widen_ord (m:=n.+1) (leqnSn n) i) \/ x \in f' ord_max
T: eqType
f: nat -> seq T
x: T
n: nat
IHn: forall (j : 'I_n) (f : 'I_n -> seq T), j < n -> x \in f j -> x \in \cat_(i<n)f i
j: 'I_n.+1
f': 'I_n.+1 -> seq T
Hx: x \in f' j
Hj: j = n

x \in \cat_(i<n)f' (widen_ord (m:=n.+1) (leqnSn n) i) \/ x \in f' ord_max
by right; rewrite (_ : ord_max = j); [|apply ord_inj].
T: eqType
f: nat -> seq T
x: T
n: nat
IHn: forall (j : 'I_n) (f : 'I_n -> seq T), j < n -> x \in f j -> x \in \cat_(i<n)f i
j: 'I_n.+1
f': 'I_n.+1 -> seq T
Hx: x \in f' j
Hj: j < n

x \in \cat_(i<n)f' (widen_ord (m:=n.+1) (leqnSn n) i) \/ x \in f' ord_max
T: eqType
f: nat -> seq T
x: T
n: nat
IHn: forall (j : 'I_n) (f : 'I_n -> seq T), j < n -> x \in f j -> x \in \cat_(i<n)f i
j: 'I_n.+1
f': 'I_n.+1 -> seq T
Hx: x \in f' j
Hj: j < n

x \in \cat_(i<n)f' (widen_ord (m:=n.+1) (leqnSn n) i)
T: eqType
f: nat -> seq T
x: T
n: nat
IHn: forall (j : 'I_n) (f : 'I_n -> seq T), j < n -> x \in f j -> x \in \cat_(i<n)f i
j: 'I_n.+1
f': 'I_n.+1 -> seq T
Hx: x \in f' j
Hj: j < n

x \in f' (widen_ord (m:=n.+1) (leqnSn n) (Ordinal (n:=n) (m:=j) Hj))
by set j' := widen_ord _ _; have -> : j' = j; [apply ord_inj|]. Qed. End BigCatNatElements. (** In this section, we show how we can preserve uniqueness of the elements (i.e. the absence of a duplicate) over a concatenation of sequences. *) Section BigCatNatDistinctElements. (** Assume that there are no duplicates in each of the possible sequences to concatenate... *) Hypothesis H_uniq_seq : forall i, uniq (f i). (** ...and that there are no elements in common between the sequences. *) Hypothesis H_no_elements_in_common : forall x i1 i2, x \in f i1 -> x \in f i2 -> i1 = i2. (** We prove that the concatenation will yield a sequence with unique elements. *)
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2

forall n1 n2 : nat, uniq (\cat_(n1<=i<n2)f i)
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2

forall n1 n2 : nat, uniq (\cat_(n1<=i<n2)f i)
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2: nat

uniq (\cat_(n1<=i<n2)f i)
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2: nat
LE: n1 <= n2

uniq (\cat_(n1<=i<n2)f i)
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2: nat
LE: n1 <= n2

uniq (\cat_(n1<=i<n1 + n2 - n1)f i)
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2: nat
LE: n1 <= n2
delta:= n2 - n1: nat

uniq (\cat_(n1<=i<n1 + delta)f i)
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2: nat
LE: n1 <= n2
delta: nat
IHdelta: uniq (\cat_(n1<=i<n1 + delta)f i)

uniq (\cat_(n1<=i<n1 + delta.+1)f i)
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2: nat
LE: n1 <= n2
delta: nat
IHdelta: uniq (\cat_(n1<=i<n1 + delta)f i)

uniq (\cat_(n1<=i<n1 + delta)f i ++ f (n1 + delta))
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2: nat
LE: n1 <= n2
delta: nat
IHdelta: uniq (\cat_(n1<=i<n1 + delta)f i)

~~ has [in \cat_(n1<=i<n1 + delta)f i] (f (n1 + delta)) && uniq (f (n1 + delta))
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2: nat
LE: n1 <= n2
delta: nat
IHdelta: uniq (\cat_(n1<=i<n1 + delta)f i)

~~ has [in \cat_(n1<=i<n1 + delta)f i] (f (n1 + delta))
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2: nat
LE: n1 <= n2
delta: nat
IHdelta: uniq (\cat_(n1<=i<n1 + delta)f i)
x: T
INx: x \in f (n1 + delta)

[predC \cat_(n1<=i<n1 + delta)f i] x
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2: nat
LE: n1 <= n2
delta: nat
IHdelta: uniq (\cat_(n1<=i<n1 + delta)f i)
x: T
INx: x \in f (n1 + delta)
BUG: x \in \cat_(n1<=i<n1 + delta)f i

False
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2: nat
LE: n1 <= n2
delta: nat
IHdelta: uniq (\cat_(n1<=i<n1 + delta)f i)
x: T
INx: x \in f (n1 + delta)
BUG: exists i : nat, x \in f i /\ n1 <= i < n1 + delta

False
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2: nat
LE: n1 <= n2
delta: nat
IHdelta: uniq (\cat_(n1<=i<n1 + delta)f i)
x: T
INx: x \in f (n1 + delta)
i: nat
IN: x \in f i
LTi: i < n1 + delta

False
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n1, n2: nat
LE: n1 <= n2
delta: nat
IHdelta: uniq (\cat_(n1<=i<n1 + delta)f i)
x: T
i: nat
INx: i = n1 + delta
IN: x \in f i
LTi: i < n1 + delta

False
by rewrite INx ltnn in LTi. Qed. (** Conversely, if the concatenation of the sequences has no duplicates, any element can only belong to a single sequence. *)
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2

forall (n : nat) (f : 'I_n -> seq T), uniq (\cat_(i<n)f i) -> forall (x : T) (i1 i2 : 'I_n), x \in f i1 -> x \in f i2 -> i1 = i2
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2

forall (n : nat) (f : 'I_n -> seq T), uniq (\cat_(i<n)f i) -> forall (x : T) (i1 i2 : 'I_n), x \in f i1 -> x \in f i2 -> i1 = i2
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat

forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_1 -> seq T
Huniq: uniq (\cat_(i<1)f' i)
x: T
i1, i2: 'I_1
Hi1: x \in f' i1
Hi2: x \in f' i2

i1 = i2
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
Huniq: uniq (\cat_(i<n.+2)f' i)
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
i1 = i2
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_1 -> seq T
Huniq: uniq (\cat_(i<1)f' i)
x: T
i1, i2: 'I_1
Hi1: x \in f' i1
Hi2: x \in f' i2

i1 = i2
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_1 -> seq T
Huniq: uniq (\cat_(i<1)f' i)
x: T
i1, i2: 0 < 1

Ordinal (n:=1) (m:=0) i1 = Ordinal (n:=1) (m:=0) i2
apply f_equal, eq_irrelevance.
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
Huniq: uniq (\cat_(i<n.+2)f' i)
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2

i1 = i2
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
Huniq: uniq (\cat_(i<n.+2)f' i)
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 == n.+1

i1 = i2
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
Huniq: uniq (\cat_(i<n.+2)f' i)
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
i1 = i2
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
Huniq: uniq (\cat_(i<n.+2)f' i)
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 == n.+1
H'i2: i2 == n.+1

i1 = i2
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
Huniq: uniq (\cat_(i<n.+2)f' i)
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 == n.+1
H'i2: i2 < n.+1
i1 = i2
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
Huniq: uniq (\cat_(i<n.+2)f' i)
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 == n.+1
i1 = i2
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
Huniq: uniq (\cat_(i<n.+2)f' i)
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 < n.+1
i1 = i2
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
Huniq: uniq (\cat_(i<n.+2)f' i)
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 == n.+1
H'i2: i2 == n.+1

i1 = i2
by apply ord_inj; move: H'i1 H'i2 => /eqP -> /eqP ->.
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
Huniq: uniq (\cat_(i<n.+2)f' i)
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 == n.+1
H'i2: i2 < n.+1

i1 = i2
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
Huniq: uniq (\cat_(i<n.+2)f' i)
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 == n.+1
i1 = i2
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
Huniq: uniq (\cat_(i<n.+2)f' i)
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 < n.+1
i1 = i2
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
Huniq: uniq (\cat_(i<n.+2)f' i)
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 == n.+1
H'i2: i2 < n.+1

i1 = i2
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
Huniq: uniq (\cat_(i<n.+2)f' i)
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 == n.+1
H'i2: i2 < n.+1

False
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 == n.+1
H'i2: i2 < n.+1
H: ~~ has [in \big[seq_cat__canonical__Monoid_Law T/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)] (f' ord_max)

False
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 == n.+1
H'i2: i2 < n.+1

has [in \big[seq_cat__canonical__Monoid_Law T/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)] (f' ord_max)
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 == n.+1
H'i2: i2 < n.+1

x \in f' ord_max
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 == n.+1
H'i2: i2 < n.+1
x \in \cat_(i<n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 == n.+1
H'i2: i2 < n.+1

x \in f' ord_max
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 == n.+1
H'i2: i2 < n.+1
o:= ord_max: 'I_n.+2

o = i1
by apply ord_inj; move: H'i1 => /eqP ->.
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 == n.+1
H'i2: i2 < n.+1

x \in \cat_(i<n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 == n.+1
H'i2: i2 < n.+1

x \in f' (widen_ord (m:=n.+2) (leqnSn n.+1) (Ordinal (n:=n.+1) (m:=i2) H'i2))
by set o := widen_ord _ _; suff -> : o = i2; [|apply ord_inj].
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
Huniq: uniq (\cat_(i<n.+2)f' i)
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 == n.+1

i1 = i2
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
Huniq: uniq (\cat_(i<n.+2)f' i)
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 < n.+1
i1 = i2
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
Huniq: uniq (\cat_(i<n.+2)f' i)
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 == n.+1

i1 = i2
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
Huniq: uniq (\cat_(i<n.+2)f' i)
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 == n.+1

False
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 == n.+1
H: ~~ has [in \big[seq_cat__canonical__Monoid_Law T/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)] (f' ord_max)

False
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 == n.+1

has [in \big[seq_cat__canonical__Monoid_Law T/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)] (f' ord_max)
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 == n.+1

x \in f' ord_max
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 == n.+1
x \in \cat_(i<n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 == n.+1

x \in f' ord_max
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 == n.+1
o:= ord_max: 'I_n.+2

o = i2
by apply ord_inj; move: H'i2 => /eqP ->.
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 == n.+1

x \in \cat_(i<n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 == n.+1

x \in f' (widen_ord (m:=n.+2) (leqnSn n.+1) (Ordinal (n:=n.+1) (m:=i1) H'i1))
by set o := widen_ord _ _; suff -> : o = i1; [|apply ord_inj].
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
Huniq: uniq (\cat_(i<n.+2)f' i)
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 < n.+1

i1 = i2
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 < n.+1
Huniq: uniq (\big[seq_cat__canonical__Monoid_Law T/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i))

i1 = i2
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 < n.+1
Huniq: uniq (\big[seq_cat__canonical__Monoid_Law T/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i))

inord i1 = inord i2
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 < n.+1
Huniq: uniq (\big[seq_cat__canonical__Monoid_Law T/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i))

x \in f' (widen_ord (m:=n.+2) (leqnSn n.+1) (inord i1))
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 < n.+1
Huniq: uniq (\big[seq_cat__canonical__Monoid_Law T/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i))
x \in f' (widen_ord (m:=n.+2) (leqnSn n.+1) (inord i2))
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 < n.+1
Huniq: uniq (\big[seq_cat__canonical__Monoid_Law T/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i))

x \in f' (widen_ord (m:=n.+2) (leqnSn n.+1) (inord i1))
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 < n.+1
Huniq: uniq (\big[seq_cat__canonical__Monoid_Law T/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i))
i1':= widen_ord (m:=n.+2) (leqnSn n.+1) (inord i1): 'I_n.+2

i1' = i1
by apply ord_inj; rewrite /= inordK.
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 < n.+1
Huniq: uniq (\big[seq_cat__canonical__Monoid_Law T/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i))

x \in f' (widen_ord (m:=n.+2) (leqnSn n.+1) (inord i2))
T: eqType
f: nat -> seq T
H_uniq_seq: forall i : nat, uniq (f i)
H_no_elements_in_common: forall (x : T) (i1 i2 : nat), x \in f i1 -> x \in f i2 -> i1 = i2
n: nat
IHn: forall f : 'I_n.+1 -> seq T, uniq (\cat_(i<n.+1)f i) -> forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
f': 'I_n.+2 -> seq T
x: T
i1, i2: 'I_n.+2
Hi1: x \in f' i1
Hi2: x \in f' i2
H'i1: i1 < n.+1
H'i2: i2 < n.+1
Huniq: uniq (\big[seq_cat__canonical__Monoid_Law T/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i))
i2':= widen_ord (m:=n.+2) (leqnSn n.+1) (inord i2): 'I_n.+2

i2' = i2
by apply ord_inj; rewrite /= inordK. Qed. End BigCatNatDistinctElements. (** We show that filtering a concatenated sequence by any predicate [P] is the same as concatenating the elements of the sequence that satisfy [P]. *)
T: eqType
f: nat -> seq T

forall (X : Type) (F : nat -> seq X) (P : X -> bool) (t1 t2 : nat), [seq x <- \cat_(t1<=t<t2)F t | P x] = \cat_(t1<=t<t2)[seq x <- F t | P x]
T: eqType
f: nat -> seq T

forall (X : Type) (F : nat -> seq X) (P : X -> bool) (t1 t2 : nat), [seq x <- \cat_(t1<=t<t2)F t | P x] = \cat_(t1<=t<t2)[seq x <- F t | P x]
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
P: X -> bool
t1, t2: nat

[seq x <- \cat_(t1<=t<t2)F t | P x] = \cat_(t1<=t<t2)[seq x <- F t | P x]
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
P: X -> bool
t1, t2: nat
T1_LT: t1 <= t2

[seq x <- \cat_(t1<=t<t2)F t | P x] = \cat_(t1<=t<t2)[seq x <- F t | P x]
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
P: X -> bool
t1, t2: nat
T2_LT: t2 <= t1
[seq x <- \cat_(t1<=t<t2)F t | P x] = \cat_(t1<=t<t2)[seq x <- F t | P x]
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
P: X -> bool
t1, t2: nat
T1_LT: t1 <= t2

[seq x <- \cat_(t1<=t<t2)F t | P x] = \cat_(t1<=t<t2)[seq x <- F t | P x]
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
P: X -> bool
t1, t2: nat
T1_LT: t1 <= t2
EX: exists Δ : nat, t2 = t1 + Δ

[seq x <- \cat_(t1<=t<t2)F t | P x] = \cat_(t1<=t<t2)[seq x <- F t | P x]
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
P: X -> bool
t1, Δ: nat
T1_LT: t1 <= t1 + Δ

[seq x <- \cat_(t1<=t<t1 + Δ)F t | P x] = \cat_(t1<=t<t1 + Δ)[seq x <- F t | P x]
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
P: X -> bool
t1: nat
T1_LT: t1 <= t1 + 0

[seq x <- \cat_(t1<=t<t1 + 0)F t | P x] = \cat_(t1<=t<t1 + 0)[seq x <- F t | P x]
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
P: X -> bool
t1, Δ: nat
IHΔ: t1 <= t1 + Δ -> [seq x <- \cat_(t1<=t<t1 + Δ)F t | P x] = \cat_(t1<=t<t1 + Δ)[seq x <- F t | P x]
T1_LT: t1 <= t1 + Δ.+1
[seq x <- \cat_(t1<=t<t1 + Δ.+1)F t | P x] = \cat_(t1<=t<t1 + Δ.+1)[seq x <- F t | P x]
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
P: X -> bool
t1: nat
T1_LT: t1 <= t1 + 0

[seq x <- \cat_(t1<=t<t1 + 0)F t | P x] = \cat_(t1<=t<t1 + 0)[seq x <- F t | P x]
by rewrite addn0 !big_geq => //.
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
P: X -> bool
t1, Δ: nat
IHΔ: t1 <= t1 + Δ -> [seq x <- \cat_(t1<=t<t1 + Δ)F t | P x] = \cat_(t1<=t<t1 + Δ)[seq x <- F t | P x]
T1_LT: t1 <= t1 + Δ.+1

[seq x <- \cat_(t1<=t<t1 + Δ.+1)F t | P x] = \cat_(t1<=t<t1 + Δ.+1)[seq x <- F t | P x]
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
P: X -> bool
t1, Δ: nat
IHΔ: t1 <= t1 + Δ -> [seq x <- \cat_(t1<=t<t1 + Δ)F t | P x] = \cat_(t1<=t<t1 + Δ)[seq x <- F t | P x]
T1_LT: t1 <= t1 + Δ.+1

[seq x <- \cat_(t1<=t<t1 + Δ.+1)F t | P x] = \cat_(t1<=t<t1 + Δ.+1)[seq x <- F t | P x]
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
P: X -> bool
t1, Δ: nat
IHΔ: t1 <= t1 + Δ -> [seq x <- \cat_(t1<=t<t1 + Δ)F t | P x] = \cat_(t1<=t<t1 + Δ)[seq x <- F t | P x]
T1_LT: t1 <= t1 + Δ.+1

[seq x <- \cat_(t1<=i<t1 + Δ)F i ++ F (t1 + Δ) | P x] = \cat_(t1<=i<t1 + Δ)[seq x <- F i | P x] ++ [seq x <- F (t1 + Δ) | P x]
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
P: X -> bool
t1, Δ: nat
IHΔ: t1 <= t1 + Δ -> [seq x <- \cat_(t1<=t<t1 + Δ)F t | P x] = \cat_(t1<=t<t1 + Δ)[seq x <- F t | P x]
T1_LT: t1 <= t1 + Δ.+1

t1 <= t1 + Δ
by lia. }
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
P: X -> bool
t1, t2: nat
T2_LT: t2 <= t1

[seq x <- \cat_(t1<=t<t2)F t | P x] = \cat_(t1<=t<t2)[seq x <- F t | P x]
by rewrite !big_geq => //. Qed. (** We show that the size of a concatenated sequence is the same as summation of sizes of each element of the sequence. *)
T: eqType
f: nat -> seq T

forall (X : Type) (F : nat -> seq X) (t1 t2 : nat), \sum_(t1 <= t < t2) size (F t) = size (\cat_(t1<=t<t2)F t)
T: eqType
f: nat -> seq T

forall (X : Type) (F : nat -> seq X) (t1 t2 : nat), \sum_(t1 <= t < t2) size (F t) = size (\cat_(t1<=t<t2)F t)
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
t1, t2: nat

\sum_(t1 <= t < t2) size (F t) = size (\cat_(t1<=t<t2)F t)
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
t1, t2: nat
T1_LT: t1 <= t2

\sum_(t1 <= t < t2) size (F t) = size (\cat_(t1<=t<t2)F t)
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
t1, t2: nat
T2_LT: t2 <= t1
\sum_(t1 <= t < t2) size (F t) = size (\cat_(t1<=t<t2)F t)
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
t1, t2: nat
T1_LT: t1 <= t2

\sum_(t1 <= t < t2) size (F t) = size (\cat_(t1<=t<t2)F t)
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
t1, t2: nat
T1_LT: t1 <= t2
EX: exists Δ : nat, t2 = t1 + Δ

\sum_(t1 <= t < t2) size (F t) = size (\cat_(t1<=t<t2)F t)
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
t1, Δ: nat
T1_LT: t1 <= t1 + Δ

\sum_(t1 <= t < t1 + Δ) size (F t) = size (\cat_(t1<=t<t1 + Δ)F t)
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
t1: nat
T1_LT: t1 <= t1 + 0

\sum_(t1 <= t < t1 + 0) size (F t) = size (\cat_(t1<=t<t1 + 0)F t)
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
t1, Δ: nat
IHΔ: t1 <= t1 + Δ -> \sum_(t1 <= t < t1 + Δ) size (F t) = size (\cat_(t1<=t<t1 + Δ)F t)
T1_LT: t1 <= t1 + Δ.+1
\sum_(t1 <= t < t1 + Δ.+1) size (F t) = size (\cat_(t1<=t<t1 + Δ.+1)F t)
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
t1: nat
T1_LT: t1 <= t1 + 0

\sum_(t1 <= t < t1 + 0) size (F t) = size (\cat_(t1<=t<t1 + 0)F t)
by rewrite addn0 !big_geq => //.
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
t1, Δ: nat
IHΔ: t1 <= t1 + Δ -> \sum_(t1 <= t < t1 + Δ) size (F t) = size (\cat_(t1<=t<t1 + Δ)F t)
T1_LT: t1 <= t1 + Δ.+1

\sum_(t1 <= t < t1 + Δ.+1) size (F t) = size (\cat_(t1<=t<t1 + Δ.+1)F t)
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
t1, Δ: nat
IHΔ: t1 <= t1 + Δ -> \sum_(t1 <= t < t1 + Δ) size (F t) = size (\cat_(t1<=t<t1 + Δ)F t)
T1_LT: t1 <= t1 + Δ.+1

\sum_(t1 <= t < t1 + Δ.+1) size (F t) = size (\cat_(t1<=t<t1 + Δ.+1)F t)
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
t1, Δ: nat
IHΔ: t1 <= t1 + Δ -> \sum_(t1 <= t < t1 + Δ) size (F t) = size (\cat_(t1<=t<t1 + Δ)F t)
T1_LT: t1 <= t1 + Δ.+1

\sum_(t1 <= i < t1 + Δ) size (F i) + size (F (t1 + Δ)) = size (\cat_(t1<=i<t1 + Δ)F i ++ F (t1 + Δ))
by rewrite size_cat IHΔ => //; lia. }
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
t1, t2: nat
T2_LT: t2 <= t1

\sum_(t1 <= t < t2) size (F t) = size (\cat_(t1<=t<t2)F t)
by rewrite !big_geq => //. Qed. End BigCatNatLemmas. (** In this section, we introduce a few lemmas about the concatenation operation performed over arbitrary sequences. *) Section BigCatLemmas. (** Consider any two types [X] and [Y] supporting equality comparisons... *) Variable X Y : eqType. (** ...and a function [f] that, given an index [X], yields a sequence of [Y]. *) Variable f : X -> seq Y. (** First, we show that the concatenation comprises all the elements of each sequence; i.e. any element contained in one of the sequences will also be an element of the result of the concatenation. *)
X, Y: eqType
f: X -> seq Y

forall (x : X) (y : Y) (s : seq_predType X), x \in s -> y \in f x -> y \in \cat_(x0<-s)f x0
X, Y: eqType
f: X -> seq Y

forall (x : X) (y : Y) (s : seq_predType X), x \in s -> y \in f x -> y \in \cat_(x0<-s)f x0
X, Y: eqType
f: X -> seq Y
x: X
y: Y
s: seq_predType X
INs: x \in s
INfx: y \in f x

y \in \cat_(x<-s)f x
X, Y: eqType
f: X -> seq Y
x: X
y: Y
INfx: y \in f x
z: X
s: seq X
IHs: x \in s -> y \in \cat_(x<-s)f x
INs: x \in z :: s

y \in \cat_(x<-(z :: s))f x
X, Y: eqType
f: X -> seq Y
x: X
y: Y
INfx: y \in f x
z: X
s: seq X
IHs: x \in s -> y \in \cat_(x<-s)f x
INs: x \in z :: s

(y \in f z) || (y \in \cat_(j<-s)f j)
X, Y: eqType
f: X -> seq Y
x: X
y: Y
INfx: y \in f x
z: X
s: seq X
IHs: x \in s -> y \in \cat_(x<-s)f x
HEAD: x = z

(y \in f z) || (y \in \cat_(j<-s)f j)
X, Y: eqType
f: X -> seq Y
x: X
y: Y
INfx: y \in f x
z: X
s: seq X
IHs: x \in s -> y \in \cat_(x<-s)f x
CONS: x \in s
(y \in f z) || (y \in \cat_(j<-s)f j)
X, Y: eqType
f: X -> seq Y
x: X
y: Y
INfx: y \in f x
z: X
s: seq X
IHs: x \in s -> y \in \cat_(x<-s)f x
HEAD: x = z

(y \in f z) || (y \in \cat_(j<-s)f j)
by rewrite -HEAD; apply /orP; left.
X, Y: eqType
f: X -> seq Y
x: X
y: Y
INfx: y \in f x
z: X
s: seq X
IHs: x \in s -> y \in \cat_(x<-s)f x
CONS: x \in s

(y \in f z) || (y \in \cat_(j<-s)f j)
by apply /orP; right; apply IHs. Qed. (** Conversely, we prove that any element belonging to a concatenation of sequences must come from one of the sequences. *)
X, Y: eqType
f: X -> seq Y

forall (P : X -> bool) (s : seq X) (y : Y), y \in \cat_(x<-s|P x)f x -> exists x : X, x \in s /\ y \in f x
X, Y: eqType
f: X -> seq Y

forall (P : X -> bool) (s : seq X) (y : Y), y \in \cat_(x<-s|P x)f x -> exists x : X, x \in s /\ y \in f x
X, Y: eqType
f: X -> seq Y
P: X -> bool

forall (s : seq X) (y : Y), y \in \cat_(x<-s|P x)f x -> exists x : X, x \in s /\ y \in f x
X, Y: eqType
f: X -> seq Y
P: X -> bool
a: X
s: seq X
IHs: forall y : Y, y \in \cat_(x<-s|P x)f x -> exists x : X, x \in s /\ y \in f x
y: Y

y \in \cat_(x<-(a :: s)|P x)f x -> exists x : X, x \in a :: s /\ y \in f x
X, Y: eqType
f: X -> seq Y
P: X -> bool
a: X
s: seq X
IHs: forall y : Y, y \in \cat_(x<-s|P x)f x -> exists x : X, x \in s /\ y \in f x
y: Y

y \in (if P a then f a ++ \cat_(j<-s|P j)f j else \cat_(j<-s|P j)f j) -> exists x : X, x \in a :: s /\ y \in f x
X, Y: eqType
f: X -> seq Y
P: X -> bool
a: X
s: seq X
IHs: forall y : Y, y \in \cat_(x<-s|P x)f x -> exists x : X, x \in s /\ y \in f x
y: Y

y \in f a ++ \cat_(j<-s|P j)f j -> exists x : X, x \in a :: s /\ y \in f x
X, Y: eqType
f: X -> seq Y
P: X -> bool
a: X
s: seq X
IHs: forall y : Y, y \in \cat_(x<-s|P x)f x -> exists x : X, x \in s /\ y \in f x
y: Y
HEAD: y \in f a

exists x : X, x \in a :: s /\ y \in f x
X, Y: eqType
f: X -> seq Y
P: X -> bool
a: X
s: seq X
IHs: forall y : Y, y \in \cat_(x<-s|P x)f x -> exists x : X, x \in s /\ y \in f x
y: Y
CONS: y \in \cat_(j<-s|P j)f j
exists x : X, x \in a :: s /\ y \in f x
X, Y: eqType
f: X -> seq Y
P: X -> bool
a: X
s: seq X
IHs: forall y : Y, y \in \cat_(x<-s|P x)f x -> exists x : X, x \in s /\ y \in f x
y: Y
HEAD: y \in f a

exists x : X, x \in a :: s /\ y \in f x
X, Y: eqType
f: X -> seq Y
P: X -> bool
a: X
s: seq X
IHs: forall y : Y, y \in \cat_(x<-s|P x)f x -> exists x : X, x \in s /\ y \in f x
y: Y
HEAD: y \in f a

a \in a :: s /\ y \in f a
by split => //; apply mem_head.
X, Y: eqType
f: X -> seq Y
P: X -> bool
a: X
s: seq X
IHs: forall y : Y, y \in \cat_(x<-s|P x)f x -> exists x : X, x \in s /\ y \in f x
y: Y
CONS: y \in \cat_(j<-s|P j)f j

exists x : X, x \in a :: s /\ y \in f x
X, Y: eqType
f: X -> seq Y
P: X -> bool
a: X
s: seq X
IHs: forall y : Y, y \in \cat_(x<-s|P x)f x -> exists x : X, x \in s /\ y \in f x
y: Y
CONS: y \in \cat_(j<-s|P j)f j
x: X
INs: x \in s
INfx: y \in f x

exists x : X, x \in a :: s /\ y \in f x
X, Y: eqType
f: X -> seq Y
P: X -> bool
a: X
s: seq X
IHs: forall y : Y, y \in \cat_(x<-s|P x)f x -> exists x : X, x \in s /\ y \in f x
y: Y
CONS: y \in \cat_(j<-s|P j)f j
x: X
INs: x \in s
INfx: y \in f x

x \in a :: s
by rewrite in_cons; apply /orP; right. Qed. (** Next, we show that a map and filter operation can be done either before or after a concatenation, leading to the same result. *)
X, Y: eqType
f: X -> seq Y

forall (xss : seq X) (P : Y -> bool), [seq x <- \cat_(xs<-xss)f xs | P x] = \cat_(xs<-xss)[seq x <- f xs | P x]
X, Y: eqType
f: X -> seq Y

forall (xss : seq X) (P : Y -> bool), [seq x <- \cat_(xs<-xss)f xs | P x] = \cat_(xs<-xss)[seq x <- f xs | P x]
X, Y: eqType
f: X -> seq Y
xss: seq X
P: Y -> bool

[seq x <- \cat_(xs<-xss)f xs | P x] = \cat_(xs<-xss)[seq x <- f xs | P x]
X, Y: eqType
f: X -> seq Y
P: Y -> bool

[seq x <- \cat_(xs<-[::])f xs | P x] = \cat_(xs<-[::])[seq x <- f xs | P x]
X, Y: eqType
f: X -> seq Y
P: Y -> bool
a: X
xss: seq X
IHxss: [seq x <- \cat_(xs<-xss)f xs | P x] = \cat_(xs<-xss)[seq x <- f xs | P x]
[seq x <- \cat_(xs<-(a :: xss))f xs | P x] = \cat_(xs<-(a :: xss))[seq x <- f xs | P x]
X, Y: eqType
f: X -> seq Y
P: Y -> bool

[seq x <- \cat_(xs<-[::])f xs | P x] = \cat_(xs<-[::])[seq x <- f xs | P x]
by rewrite !big_nil.
X, Y: eqType
f: X -> seq Y
P: Y -> bool
a: X
xss: seq X
IHxss: [seq x <- \cat_(xs<-xss)f xs | P x] = \cat_(xs<-xss)[seq x <- f xs | P x]

[seq x <- \cat_(xs<-(a :: xss))f xs | P x] = \cat_(xs<-(a :: xss))[seq x <- f xs | P x]
by rewrite !big_cons filter_cat IHxss. Qed. (** In this section, we show how we can preserve uniqueness of the elements (i.e. the absence of a duplicate) over a concatenation of sequences. *) Section BigCatDistinctElements. (** Consider a list [xs], ... *) Context {xs : seq X}. (** ... a filter predicate [P], ... *) Context {P : pred X}. (** ... assume that there are no duplicates in each of the possible sequences to concatenate... *) Hypothesis H_uniq_f : forall x, P x -> uniq (f x). (** ...and that there are no elements in common between the sequences. *) Hypothesis H_no_elements_in_common : forall x y z, x \in f y -> x \in f z -> y = z. (** We prove that the concatenation will yield a sequence with unique elements. *)
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P x -> uniq (f x)
H_no_elements_in_common: forall (x : Y) (y z : X), x \in f y -> x \in f z -> y = z

uniq xs -> uniq (\cat_(x<-xs|P x)f x)
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P x -> uniq (f x)
H_no_elements_in_common: forall (x : Y) (y z : X), x \in f y -> x \in f z -> y = z

uniq xs -> uniq (\cat_(x<-xs|P x)f x)
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P x -> uniq (f x)
H_no_elements_in_common: forall (x : Y) (y z : X), x \in f y -> x \in f z -> y = z

forall xs : seq X, uniq xs -> uniq (\cat_(x<-xs|P x)f x)
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P x -> uniq (f x)
H_no_elements_in_common: forall (x : Y) (y z : X), x \in f y -> x \in f z -> y = z
a: X
xs': seq X
IHxs: uniq xs' -> uniq (\cat_(x<-xs'|P x)f x)

uniq (a :: xs') -> uniq (\cat_(x<-(a :: xs')|P x)f x)
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P x -> uniq (f x)
H_no_elements_in_common: forall (x : Y) (y z : X), x \in f y -> x \in f z -> y = z
a: X
xs': seq X
IHxs: uniq xs' -> uniq (\cat_(x<-xs'|P x)f x)
NINxs: a \notin xs'
UNIQ: uniq xs'

uniq (\cat_(x<-(a :: xs')|P x)f x)
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P x -> uniq (f x)
H_no_elements_in_common: forall (x : Y) (y z : X), x \in f y -> x \in f z -> y = z
a: X
xs': seq X
IHxs: uniq xs' -> uniq (\cat_(x<-xs'|P x)f x)
NINxs: a \notin xs'
UNIQ: uniq xs'

uniq (if P a then f a ++ \cat_(j<-xs'|P j)f j else \cat_(j<-xs'|P j)f j)
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P x -> uniq (f x)
H_no_elements_in_common: forall (x : Y) (y z : X), x \in f y -> x \in f z -> y = z
a: X
xs': seq X
IHxs: uniq xs' -> uniq (\cat_(x<-xs'|P x)f x)
NINxs: a \notin xs'
UNIQ: uniq xs'
Pa: P a = true

uniq (f a ++ \cat_(j<-xs'|P j)f j)
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P x -> uniq (f x)
H_no_elements_in_common: forall (x : Y) (y z : X), x \in f y -> x \in f z -> y = z
a: X
xs': seq X
IHxs: uniq xs' -> uniq (\cat_(x<-xs'|P x)f x)
NINxs: a \notin xs'
UNIQ: uniq xs'
Pa: P a = true

[&& uniq (f a), ~~ has [in f a] (\cat_(j<-xs'|P j)f j) & uniq (\cat_(j<-xs'|P j)f j)]
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P x -> uniq (f x)
H_no_elements_in_common: forall (x : Y) (y z : X), x \in f y -> x \in f z -> y = z
a: X
xs': seq X
IHxs: uniq xs' -> uniq (\cat_(x<-xs'|P x)f x)
NINxs: a \notin xs'
UNIQ: uniq xs'
Pa: P a = true

~~ has [in f a] (\cat_(j<-xs'|P j)f j) && uniq (\cat_(j<-xs'|P j)f j)
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P x -> uniq (f x)
H_no_elements_in_common: forall (x : Y) (y z : X), x \in f y -> x \in f z -> y = z
a: X
xs': seq X
IHxs: uniq xs' -> uniq (\cat_(x<-xs'|P x)f x)
NINxs: a \notin xs'
UNIQ: uniq xs'
Pa: P a = true

~~ has [in f a] (\cat_(j<-xs'|P j)f j)
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P x -> uniq (f x)
H_no_elements_in_common: forall (x : Y) (y z : X), x \in f y -> x \in f z -> y = z
a: X
xs': seq X
IHxs: uniq xs' -> uniq (\cat_(x<-xs'|P x)f x)
NINxs: a \notin xs'
UNIQ: uniq xs'
Pa: P a = true
x: Y
IN: x \in \cat_(j<-xs'|P j)f j
INfa: x \in f a

False
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P x -> uniq (f x)
H_no_elements_in_common: forall (x : Y) (y z : X), x \in f y -> x \in f z -> y = z
a: X
xs': seq X
IHxs: uniq xs' -> uniq (\cat_(x<-xs'|P x)f x)
NINxs: a \notin xs'
UNIQ: uniq xs'
Pa: P a = true
x: Y
IN: x \in \cat_(j<-xs'|P j)f j
INfa: x \in f a
a': X
INxs: a' \in xs'
INfa': x \in f a'

False
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P x -> uniq (f x)
H_no_elements_in_common: forall (x : Y) (y z : X), x \in f y -> x \in f z -> y = z
a: X
xs': seq X
IHxs: uniq xs' -> uniq (\cat_(x<-xs'|P x)f x)
NINxs: a \notin xs'
UNIQ: uniq xs'
Pa: P a = true
x: Y
IN: x \in \cat_(j<-xs'|P j)f j
INfa: x \in f a
a': X
INxs: a' \in xs'
INfa': x \in f a'
EQa: a = a'

False
by move: NINxs; rewrite EQa => /negP CONTRA. Qed. End BigCatDistinctElements. (** In this section, we show some properties of the concatenation of sequences in combination with a function [g] that cancels [f]. *) Section BigCatWithCancelFunctions. (** Consider a function [g]... *) Variable g : Y -> X. (** ... and assume that [g] can cancel [f] starting from an element of the sequence [f x]. *) Hypothesis H_g_cancels_f : forall x y, y \in f x -> g y = x. (** First, we show that no element of a sequence [f x1] can be fed into [g] and obtain an element [x2] which differs from [x1]. Hence, filtering by this condition always leads to the empty sequence. *)
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x

forall x1 x2 : X, x1 != x2 -> [seq x <- f x1 | g x == x2] = [::]
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x

forall x1 x2 : X, x1 != x2 -> [seq x <- f x1 | g x == x2] = [::]
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
x1, x2: X
NEQ: ~ x1 == x2

[seq x <- f x1 | g x == x2] = [::]
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
x1, x2: X
NEQ: ~ x1 == x2

forall x : Y, x \in f x1 -> g x != x2
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
x1, x2: X
NEQ: ~ x1 == x2
y: Y
IN: y \in f x1
EQ2: g y = x2

False
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
x1, x2: X
y: Y
IN: y \in f x1
EQ2: g y = x2

x1 = x2
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
x1, x2: X
y: Y
IN: y \in f x1
EQ2: g y = x2
EQ1: g y = x1

x1 = x2
by rewrite -EQ1 -EQ2. Qed. (** Finally, assume we are given an element [y] which is contained in a duplicate-free sequence [xs]. Then, [f] is applied to each element of [xs], but only the elements for which [g] yields [y] are kept. In this scenario, concatenating the resulting sequences will always lead to [f y]. *)
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x

forall (y : X) (xs : seq_predType X), y \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x

forall (y : X) (xs : seq_predType X), y \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
y: X
xs: seq_predType X
IN: y \in xs
UNI: uniq xs

\cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
y, x': X
xs: seq X
IHxs: y \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
IN: y \in x' :: xs
UNI: uniq (x' :: xs)

\cat_(x<-(x' :: xs))[seq x' <- f x | g x' == y] = f y
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
y, x': X
xs: seq X
IHxs: y \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
UNI: uniq (x' :: xs)
EQ: y = x'

\cat_(x<-(x' :: xs))[seq x' <- f x | g x' == y] = f y
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
y, x': X
xs: seq X
IHxs: y \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
UNI: uniq (x' :: xs)
IN: y \in xs
\cat_(x<-(x' :: xs))[seq x' <- f x | g x' == y] = f y
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
y, x': X
xs: seq X
IHxs: y \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
UNI: uniq (x' :: xs)
EQ: y = x'

\cat_(x<-(x' :: xs))[seq x' <- f x | g x' == y] = f y
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
x': X
xs: seq X
IHxs: x' \in xs -> uniq xs -> \cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] = f x'
UNI: uniq (x' :: xs)

[seq x'0 <- f x' | g x'0 == x'] ++ \cat_(j<-xs)[seq x'0 <- f j | g x'0 == x'] = f x'
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
x': X
xs: seq X
IHxs: x' \in xs -> uniq xs -> \cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] = f x'
UNI: uniq (x' :: xs)

[seq x <- f x' | g x == x'] = f x'
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
x': X
xs: seq X
IHxs: x' \in xs -> uniq xs -> \cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] = f x'
UNI: uniq (x' :: xs)
f x' ++ \cat_(j<-xs)[seq x'0 <- f j | g x'0 == x'] = f x'
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
x': X
xs: seq X
IHxs: x' \in xs -> uniq xs -> \cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] = f x'
UNI: uniq (x' :: xs)

[seq x <- f x' | g x == x'] = f x'
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
x': X
xs: seq X
IHxs: x' \in xs -> uniq xs -> \cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] = f x'
UNI: uniq (x' :: xs)

{in f x', forall x : Y, g x == x'}
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
x': X
xs: seq X
IHxs: x' \in xs -> uniq xs -> \cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] = f x'
UNI: uniq (x' :: xs)
y: Y
IN: y \in f x'

g y = x'
by apply H_g_cancels_f.
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
x': X
xs: seq X
IHxs: x' \in xs -> uniq xs -> \cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] = f x'
UNI: uniq (x' :: xs)

f x' ++ \cat_(j<-xs)[seq x'0 <- f j | g x'0 == x'] = f x'
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
x': X
xs: seq X
IHxs: x' \in xs -> uniq xs -> \cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] = f x'
UNI: uniq (x' :: xs)

\cat_(j<-xs)[seq x <- f j | g x == x'] = [::]
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
x': X
xs: seq X
IHxs: x' \in xs -> uniq xs -> \cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] = f x'
UNI: uniq (x' :: xs)
xs2: X
IN: xs2 \in xs

[seq x <- f xs2 | g x == x'] = [::]
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
x': X
xs: seq X
IHxs: x' \in xs -> uniq xs -> \cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] = f x'
UNI: uniq (x' :: xs)
xs2: X
IN: xs2 \in xs

xs2 != x'
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
xs: seq X
xs2: X
UNI: uniq (xs2 :: xs)
IHxs: xs2 \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == xs2] = f xs2
IN: xs2 \in xs

False
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
xs: seq X
xs2: X
IHxs: xs2 \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == xs2] = f xs2
IN: xs2 \in xs
NIN: xs2 \notin xs

False
by move: NIN => /negP NIN; apply: NIN.
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
y, x': X
xs: seq X
IHxs: y \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
UNI: uniq (x' :: xs)
IN: y \in xs

\cat_(x<-(x' :: xs))[seq x' <- f x | g x' == y] = f y
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
y, x': X
xs: seq X
IHxs: y \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
UNI: uniq (x' :: xs)
IN: y \in xs

\cat_(x<-(x' :: xs))[seq x' <- f x | g x' == y] = f y
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
y, x': X
xs: seq X
IHxs: y \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
UNI: uniq (x' :: xs)
IN: y \in xs

[seq x' <- f x' | g x' == y] ++ f y = f y
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
y, x': X
xs: seq X
IHxs: y \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
UNI: uniq (x' :: xs)
IN: y \in xs

x' != y
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
y: X
xs: seq X
IHxs: y \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
UNI: uniq (y :: xs)
IN: y \in xs

False
X, Y: eqType
f: X -> seq Y
g: Y -> X
H_g_cancels_f: forall (x : X) (y : Y), y \in f x -> g y = x
y: X
xs: seq X
IHxs: y \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
IN: y \in xs
NIN: y \notin xs

False
by move: NIN => /negP NIN; apply: NIN. } Qed. End BigCatWithCancelFunctions. End BigCatLemmas. (** In this section, we show that the number of elements of the result of a nested mapping and concatenation operation is independent from the order in which the concatenations are performed. *) Section BigCatNestedCount. (** Consider any three types supporting equality comparisons... *) Variable X Y Z : eqType. (** ... a function [F] that, given two indices, yields a sequence... *) Variable F : X -> Y -> seq Z. (** and a predicate [P]. *) Variable P : pred Z. (** Assume that, given two sequences [xs] and [ys], their elements are fed to [F] in a pair-wise fashion. The resulting lists are then concatenated. The following lemma shows that, when the operation described above is performed, the number of elements respecting [P] in the resulting list is the same, regardless of the order in which [xs] and [ys] are combined. *)
X, Y, Z: eqType
F: X -> Y -> seq Z
P: pred Z

forall (xs : seq X) (ys : seq Y), count P (\cat_(x<-xs)\cat_(y<-ys)F x y) = count P (\cat_(y<-ys)\cat_(x<-xs)F x y)
X, Y, Z: eqType
F: X -> Y -> seq Z
P: pred Z

forall (xs : seq X) (ys : seq Y), count P (\cat_(x<-xs)\cat_(y<-ys)F x y) = count P (\cat_(y<-ys)\cat_(x<-xs)F x y)
X, Y, Z: eqType
F: X -> Y -> seq Z
P: pred Z

count P (\cat_(x<-[::])\cat_(y<-[::])F x y) = count P (\cat_(y<-[::])\cat_(x<-[::])F x y)
X, Y, Z: eqType
F: X -> Y -> seq Z
P: pred Z
y0: Y
seqY: seq Y
IHys: count P (\cat_(x<-[::])\cat_(y<-seqY)F x y) = count P (\cat_(y<-seqY)\cat_(x<-[::])F x y)
count P (\cat_(x<-[::])\cat_(y<-(y0 :: seqY))F x y) = count P (\cat_(y<-(y0 :: seqY))\cat_(x<-[::])F x y)
X, Y, Z: eqType
F: X -> Y -> seq Z
P: pred Z
x0: X
seqX: seq X
IHxs: forall ys : seq Y, count P (\cat_(x<-seqX)\cat_(y<-ys)F x y) = count P (\cat_(y<-ys)\cat_(x<-seqX)F x y)
count P (\cat_(x<-(x0 :: seqX))\cat_(y<-[::])F x y) = count P (\cat_(y<-[::])\cat_(x<-(x0 :: seqX))F x y)
X, Y, Z: eqType
F: X -> Y -> seq Z
P: pred Z
x0: X
seqX: seq X
IHxs: forall ys : seq Y, count P (\cat_(x<-seqX)\cat_(y<-ys)F x y) = count P (\cat_(y<-ys)\cat_(x<-seqX)F x y)
y0: Y
seqY: seq Y
IHys: count P (\cat_(x<-(x0 :: seqX))\cat_(y<-seqY)F x y) = count P (\cat_(y<-seqY)\cat_(x<-(x0 :: seqX))F x y)
count P (\cat_(x<-(x0 :: seqX))\cat_(y<-(y0 :: seqY))F x y) = count P (\cat_(y<-(y0 :: seqY))\cat_(x<-(x0 :: seqX))F x y)
X, Y, Z: eqType
F: X -> Y -> seq Z
P: pred Z

count P (\cat_(x<-[::])\cat_(y<-[::])F x y) = count P (\cat_(y<-[::])\cat_(x<-[::])F x y)
by rewrite !big_nil.
X, Y, Z: eqType
F: X -> Y -> seq Z
P: pred Z
y0: Y
seqY: seq Y
IHys: count P (\cat_(x<-[::])\cat_(y<-seqY)F x y) = count P (\cat_(y<-seqY)\cat_(x<-[::])F x y)

count P (\cat_(x<-[::])\cat_(y<-(y0 :: seqY))F x y) = count P (\cat_(y<-(y0 :: seqY))\cat_(x<-[::])F x y)
X, Y, Z: eqType
F: X -> Y -> seq Z
P: pred Z
x0: X
seqX: seq X
IHxs: forall ys : seq Y, count P (\cat_(x<-seqX)\cat_(y<-ys)F x y) = count P (\cat_(y<-ys)\cat_(x<-seqX)F x y)
count P (\cat_(x<-(x0 :: seqX))\cat_(y<-[::])F x y) = count P (\cat_(y<-[::])\cat_(x<-(x0 :: seqX))F x y)
X, Y, Z: eqType
F: X -> Y -> seq Z
P: pred Z
x0: X
seqX: seq X
IHxs: forall ys : seq Y, count P (\cat_(x<-seqX)\cat_(y<-ys)F x y) = count P (\cat_(y<-ys)\cat_(x<-seqX)F x y)
y0: Y
seqY: seq Y
IHys: count P (\cat_(x<-(x0 :: seqX))\cat_(y<-seqY)F x y) = count P (\cat_(y<-seqY)\cat_(x<-(x0 :: seqX))F x y)
count P (\cat_(x<-(x0 :: seqX))\cat_(y<-(y0 :: seqY))F x y) = count P (\cat_(y<-(y0 :: seqY))\cat_(x<-(x0 :: seqX))F x y)
X, Y, Z: eqType
F: X -> Y -> seq Z
P: pred Z
y0: Y
seqY: seq Y
IHys: count P (\cat_(x<-[::])\cat_(y<-seqY)F x y) = count P (\cat_(y<-seqY)\cat_(x<-[::])F x y)

count P (\cat_(x<-[::])\cat_(y<-(y0 :: seqY))F x y) = count P (\cat_(y<-(y0 :: seqY))\cat_(x<-[::])F x y)
by rewrite big_cons count_cat -IHys !big_nil.
X, Y, Z: eqType
F: X -> Y -> seq Z
P: pred Z
x0: X
seqX: seq X
IHxs: forall ys : seq Y, count P (\cat_(x<-seqX)\cat_(y<-ys)F x y) = count P (\cat_(y<-ys)\cat_(x<-seqX)F x y)

count P (\cat_(x<-(x0 :: seqX))\cat_(y<-[::])F x y) = count P (\cat_(y<-[::])\cat_(x<-(x0 :: seqX))F x y)
X, Y, Z: eqType
F: X -> Y -> seq Z
P: pred Z
x0: X
seqX: seq X
IHxs: forall ys : seq Y, count P (\cat_(x<-seqX)\cat_(y<-ys)F x y) = count P (\cat_(y<-ys)\cat_(x<-seqX)F x y)
y0: Y
seqY: seq Y
IHys: count P (\cat_(x<-(x0 :: seqX))\cat_(y<-seqY)F x y) = count P (\cat_(y<-seqY)\cat_(x<-(x0 :: seqX))F x y)
count P (\cat_(x<-(x0 :: seqX))\cat_(y<-(y0 :: seqY))F x y) = count P (\cat_(y<-(y0 :: seqY))\cat_(x<-(x0 :: seqX))F x y)
X, Y, Z: eqType
F: X -> Y -> seq Z
P: pred Z
x0: X
seqX: seq X
IHxs: forall ys : seq Y, count P (\cat_(x<-seqX)\cat_(y<-ys)F x y) = count P (\cat_(y<-ys)\cat_(x<-seqX)F x y)

count P (\cat_(x<-(x0 :: seqX))\cat_(y<-[::])F x y) = count P (\cat_(y<-[::])\cat_(x<-(x0 :: seqX))F x y)
by rewrite big_cons count_cat IHxs !big_nil.
X, Y, Z: eqType
F: X -> Y -> seq Z
P: pred Z
x0: X
seqX: seq X
IHxs: forall ys : seq Y, count P (\cat_(x<-seqX)\cat_(y<-ys)F x y) = count P (\cat_(y<-ys)\cat_(x<-seqX)F x y)
y0: Y
seqY: seq Y
IHys: count P (\cat_(x<-(x0 :: seqX))\cat_(y<-seqY)F x y) = count P (\cat_(y<-seqY)\cat_(x<-(x0 :: seqX))F x y)

count P (\cat_(x<-(x0 :: seqX))\cat_(y<-(y0 :: seqY))F x y) = count P (\cat_(y<-(y0 :: seqY))\cat_(x<-(x0 :: seqX))F x y)
X, Y, Z: eqType
F: X -> Y -> seq Z
P: pred Z
x0: X
seqX: seq X
IHxs: forall ys : seq Y, count P (\cat_(x<-seqX)\cat_(y<-ys)F x y) = count P (\cat_(y<-ys)\cat_(x<-seqX)F x y)
y0: Y
seqY: seq Y
IHys: count P (\cat_(x<-(x0 :: seqX))\cat_(y<-seqY)F x y) = count P (\cat_(y<-seqY)\cat_(x<-(x0 :: seqX))F x y)

count P (\cat_(x<-(x0 :: seqX))\cat_(y<-(y0 :: seqY))F x y) = count P (\cat_(y<-(y0 :: seqY))\cat_(x<-(x0 :: seqX))F x y)
X, Y, Z: eqType
F: X -> Y -> seq Z
P: pred Z
x0: X
seqX: seq X
IHxs: forall ys : seq Y, count P (\cat_(x<-seqX)\cat_(y<-ys)F x y) = count P (\cat_(y<-ys)\cat_(x<-seqX)F x y)
y0: Y
seqY: seq Y
IHys: count P (\cat_(x<-(x0 :: seqX))\cat_(y<-seqY)F x y) = count P (\cat_(y<-seqY)\cat_(x<-(x0 :: seqX))F x y)

count P (F x0 y0) + count P (\cat_(j<-seqY)F x0 j) + count P (\cat_(j<-seqX)\cat_(y<-(y0 :: seqY))F j y) = count P (F x0 y0) + count P (\cat_(j<-seqX)F j y0) + count P (\cat_(j<-seqY)\cat_(x<-(x0 :: seqX))F x j)
X, Y, Z: eqType
F: X -> Y -> seq Z
P: pred Z
x0: X
seqX: seq X
IHxs: forall ys : seq Y, count P (\cat_(x<-seqX)\cat_(y<-ys)F x y) = count P (\cat_(y<-ys)\cat_(x<-seqX)F x y)
y0: Y
seqY: seq Y
IHys: count P (\cat_(x<-(x0 :: seqX))\cat_(y<-seqY)F x y) = count P (\cat_(y<-seqY)\cat_(x<-(x0 :: seqX))F x y)

count P (\cat_(j<-seqY)F x0 j) + count P (\cat_(j<-seqX)\cat_(y<-(y0 :: seqY))F j y) == count P (\cat_(j<-seqX)F j y0) + count P (\cat_(j<-seqY)\cat_(x<-(x0 :: seqX))F x j)
X, Y, Z: eqType
F: X -> Y -> seq Z
P: pred Z
x0: X
seqX: seq X
IHxs: forall ys : seq Y, count P (\cat_(x<-seqX)\cat_(y<-ys)F x y) = count P (\cat_(y<-ys)\cat_(x<-seqX)F x y)
y0: Y
seqY: seq Y
IHys: count P (\cat_(x<-(x0 :: seqX))\cat_(y<-seqY)F x y) = count P (\cat_(y<-seqY)\cat_(x<-(x0 :: seqX))F x y)

count P (\cat_(j<-seqY)F x0 j) + (count P (\cat_(x<-seqX)F x y0) + count P (\cat_(j<-seqY)\cat_(x<-seqX)F x j)) == count P (\cat_(j<-seqX)F j y0) + (count P (\cat_(y<-seqY)F x0 y) + count P (\cat_(j<-seqX)\cat_(y<-seqY)F j y))
X, Y, Z: eqType
F: X -> Y -> seq Z
P: pred Z
x0: X
seqX: seq X
IHxs: forall ys : seq Y, count P (\cat_(x<-seqX)\cat_(y<-ys)F x y) = count P (\cat_(y<-ys)\cat_(x<-seqX)F x y)
y0: Y
seqY: seq Y
IHys: count P (\cat_(x<-(x0 :: seqX))\cat_(y<-seqY)F x y) = count P (\cat_(y<-seqY)\cat_(x<-(x0 :: seqX))F x y)

count P (\cat_(j<-seqY)\cat_(x<-seqX)F x j) == count P (\cat_(j<-seqX)\cat_(y<-seqY)F j y)
by rewrite IHxs. } Qed. End BigCatNestedCount.