Theory res_quan

⊢ ∀x sos. x ∈ BIGINTER sos ⇔ ∀s::sos. x ∈ s

⊢ ∀x sos. x ∈ BIGUNION sos ⇔ ∃s::sos. x ∈ s

⊢ ∀P s. ¬(∃x::s. P x) ⇔ ∀x::s. ¬P x

⊢ ∀P s. ¬(∀x::s. P x) ⇔ ∃x::s. ¬P x

⊢ ∀p m x. x ∈ p ⇒ RES_ABSTRACT p m x = m x

⊢ ∀p m1 m2.
    (∀x. x ∈ p ⇒ m1 x = m2 x) ⇒ RES_ABSTRACT p m1 = RES_ABSTRACT p m2

⊢ ∀p m1 m2. RES_ABSTRACT p m1 = RES_ABSTRACT p m2 ⇔ ∀x. x ∈ p ⇒ m1 x = m2 x

⊢ ∀p m. RES_ABSTRACT p (RES_ABSTRACT p m) = RES_ABSTRACT p m

⊢ ∀m. RES_ABSTRACT 𝕌(:α) m = m

⊢ ∀P Q R. (∃i::(λi. P i ∨ Q i). R i) ⇔ (∃i::P. R i) ∨ ∃i::Q. R i

⊢ ∀P f. RES_EXISTS P f ⇔ ∃x. x ∈ P ∧ f x

⊢ ∀p m. RES_EXISTS p m ⇔ RES_SELECT p m ∈ p ∧ m (RES_SELECT p m)

⊢ ∀P sos. (∃x::BIGINTER sos. P x) ⇔ ∃x. (∀s::sos. x ∈ s) ∧ P x

⊢ ∀P sos. (∃x::BIGUNION sos. P x) ⇔ ∃(s::sos) (x::s). P x

⊢ ∀P s t x. (∃x::s DIFF t. P x) ⇔ ∃x::s. x ∉ t ∧ P x

⊢ ∀P Q R. (∃i::P. Q i ∨ R i) ⇔ (∃i::P. Q i) ∨ ∃i::P. R i

⊢ ∀p. ¬RES_EXISTS ∅ p

⊢ ∀P j. (∃i:: $= j. P i) ⇔ P j

⊢ ∀P s x. ¬∃s::x. F

⊢ ∀P s. RES_EXISTS s P ⇒ s ≠ ∅

⊢ ∀p m. (∃x::p. m) ⇔ p ≠ ∅ ∧ m

⊢ ∀P Q R. (∃(i::P) (j::Q). R i j) ⇔ ∃(j::Q) (i::P). R i j

⊢ ∀P s t. s ⊆ t ⇒ RES_EXISTS s P ⇒ RES_EXISTS t P

⊢ ∀P s x. (∃x::s. T) ⇔ s ≠ ∅

⊢ ∀P s t. RES_EXISTS (s ∪ t) P ⇔ RES_EXISTS s P ∨ RES_EXISTS t P

⊢ ∀P f. RES_EXISTS_UNIQUE P f ⇔ (∃x::P. f x) ∧ ∀x y::P. f x ∧ f y ⇒ x = y

⊢ ∀p m. RES_EXISTS_UNIQUE p m ⇔ ∃x::p. m x ∧ ∀y::p. m y ⇒ y = x

⊢ ∀P s. (∃!x::s. P x) ⇔ ∃!x. x ∈ s ∧ P x

⊢ ∀p. ¬RES_EXISTS_UNIQUE ∅ p

⊢ ∀P s. RES_EXISTS_UNIQUE P s ⇒ RES_EXISTS P s

⊢ ∀P s x. ¬∃!x::s. F

⊢ ∀P s. RES_EXISTS_UNIQUE s P ⇒ s ≠ ∅

⊢ ∀p m. (∃!x::p. m) ⇔ (∃x. p = {x}) ∧ m

⊢ ∀P s x. (∃!x::s. T) ⇔ ∃y. s = {y}

⊢ ∀P s x. (∃!x::s. T) ⇔ ∃!x. x ∈ s

⊢ ∀p. RES_EXISTS_UNIQUE 𝕌(:α) p ⇔ $?! p

⊢ ∀p. RES_EXISTS 𝕌(:α) p ⇔ $? p

⊢ ∀P f. RES_FORALL P f ⇔ ∀x. x ∈ P ⇒ f x

⊢ ∀P sos. (∀x::BIGINTER sos. P x) ⇔ ∀x. (∀s::sos. x ∈ s) ⇒ P x

⊢ ∀P sos. (∀x::BIGUNION sos. P x) ⇔ ∀(s::sos) (x::s). P x

⊢ ∀P Q R. (∀i::P. Q i ∧ R i) ⇔ (∀i::P. Q i) ∧ ∀i::P. R i

⊢ ∀P s t x. (∀x::s DIFF t. P x) ⇔ ∀x::s. x ∉ t ⇒ P x

⊢ ∀P Q R. (∀i::(λj. P j ∨ Q j). R i) ⇔ (∀i::P. R i) ∧ ∀i::Q. R i

⊢ ∀p. RES_FORALL ∅ p

⊢ ∀P s x. (∀x::s. F) ⇔ s = ∅

⊢ ∀P R x. (∀x (i::P). R i x) ⇔ ∀(i::P) x. R i x

⊢ ∀P s. ¬RES_FORALL s P ⇒ s ≠ ∅

⊢ ∀p m. (∀x::p. m) ⇔ p = ∅ ∨ m

⊢ ∀P Q R. (∀(i::P) (j::Q). R i j) ⇔ ∀(j::Q) (i::P). R i j

⊢ ∀P s t. s ⊆ t ⇒ RES_FORALL t P ⇒ RES_FORALL s P

⊢ ∀P s x (x::s). T

⊢ ∀P s t. RES_FORALL (s ∪ t) P ⇔ RES_FORALL s P ∧ RES_FORALL t P

⊢ ∀P j. (∀i:: $= j. P i) ⇔ P j

⊢ ∀p. RES_FORALL 𝕌(:α) p ⇔ $! p

⊢ ∀P f. RES_SELECT P f = @x. x ∈ P ∧ f x

⊢ ∀p. RES_SELECT ∅ p = @x. F

⊢ ∀p. RES_SELECT 𝕌(:α) p = $@ p