Theorems about big operators (e.g., ⋀, ⋁).

theorem TLA.bigwedge_list_nil {α : Type u} {β : Type v} (f : β → pred α) : (⋀ x ∈ [], (f x)) =tla= (⊤)

theorem TLA.bigwedge_list_cons {α : Type u} {β : Type v} (f : β → pred α) (l : List β) (b : β) : (⋀ x ∈ b :: l, (f x)) =tla= ((f b) ∧ ⋀ x ∈ l, (f x))

theorem TLA.bigwedge_list_append {α : Type u} {β : Type v} (f : β → pred α) (l1 l2 : List β) : (⋀ x ∈ l1 ++ l2, (f x)) =tla= ((⋀ x ∈ l1, (f x)) ∧ ⋀ x ∈ l2, (f x))

theorem TLA.bigwedge_forall_list {α : Type u} {β : Type v} (f : β → pred α) (l : List β) : (⋀ x ∈ l, (f x)) =tla= (∀ x, (⌞ x ∈ l ⌟ → (f x)))

theorem TLA.bigwedge_forall_fintype_list {α : Type u} {β : Type v} (f : β → pred α) (l : List β) : (⋀ x ∈ l, (f x)) =tla= (∀ x, (f l[x]))

theorem TLA.bigwedge_forall_swap {α : Type u} {β : Type v} (l : List β) {γ : Type w} (f : β → γ → pred α) : (∀ c, ⋀ x ∈ l, (f x c)) =tla= (⋀ x ∈ l, ∀ c, (f x c))

theorem TLA.bigwedge_inner_and_split {α : Type u} {β : Type v} (f g : β → pred α) (l : List β) : (⋀ x ∈ l, (f x) ∧ (g x)) =tla= ((⋀ x ∈ l, (f x)) ∧ ⋀ x ∈ l, (g x))

theorem TLA.always_bigwedge {α : Type u} {β : Type v} (f : β → pred α) (l : List β) : (□⋀ x ∈ l, (f x)) =tla= (⋀ x ∈ l, □(f x))

theorem TLA.eventually_always_bigwedge_distrib {α : Type u} {β : Type v} (f : β → pred α) (l : List β) : (◇□⋀ x ∈ l, (f x)) =tla= (⋀ x ∈ l, ◇□(f x))

theorem TLA.bigvee_list_nil {α : Type u} {β : Type v} (f : β → pred α) : (⋁ x ∈ [], (f x)) =tla= (⊥)

theorem TLA.bigvee_list_cons {α : Type u} {β : Type v} (f : β → pred α) (l : List β) (b : β) : (⋁ x ∈ b :: l, (f x)) =tla= ((f b) ∨ ⋁ x ∈ l, (f x))

theorem TLA.bigvee_exists_list {α : Type u} {β : Type v} (f : β → pred α) (l : List β) : (⋁ x ∈ l, (f x)) =tla= (∃ x, (⌞ x ∈ l ⌟ ∧ (f x)))

theorem TLA.bigvee_exists_fintype_list {α : Type u} {β : Type v} (f : β → pred α) (l : List β) : (⋁ x ∈ l, (f x)) =tla= (∃ x, (f l[x]))

theorem TLA.bigvee_and_distrib {α : Type u} {β : Type v} (f : β → pred α) (l : List β) (p : pred α) : (p ∧ ⋁ x ∈ l, (f x)) =tla= (⋁ x ∈ l, p ∧ (f x))

theorem TLA.bigwedge_bigvee_match {α : Type u} {β : Type v} (f g : β → pred α) (l : List β) : ((⋀ x ∈ l, (f x)) ∧ ⋁ x ∈ l, (g x)) |-tla- (⋁ x ∈ l, (f x) ∧ (g x))