Package hol-quotient: HOL quotient theories

Information

name	hol-quotient
version	1.1
description	HOL quotient theories
author	HOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org>
license	MIT
checksum	4d22445a191fc3d1b6250422a88ce83e01eed04b
requires	base hol-base hol-res-quan
show	Data.Bool Data.List Data.Option Data.Pair Function HOL4 Number.Natural Relation

Files

Package tarball hol-quotient-1.1.tgz
Theory source file hol-quotient.thy (included in the package tarball)

Defined Constants

HOL4
- quotient
  - quotient.-->
  - quotient.===>
  - quotient.?!!
  - quotient.respects
  - quotient.EQUIV
  - quotient.PARTIAL_EQUIV
  - quotient.QUOTIENT
  - quotient.RES_EXISTS_EQUIV
- quotient_pair
  - quotient_pair.###
- quotient_pred_set
  - quotient_pred_set.DELETER
  - quotient_pred_set.DISJOINTR
  - quotient_pred_set.FINITER
  - quotient_pred_set.GSPECR
  - quotient_pred_set.IMAGER
  - quotient_pred_set.INSERTR
  - quotient_pred_set.PSUBSETR
  - quotient_pred_set.SUBSETR
- quotient_sum
  - quotient_sum.+++
  - quotient_sum.SUM_REL_tupled

Theorems

⊦ quotient.EQUIV (=)

⊦ quotient.respects = Combinator.w

⊦ map id = id

⊦ list.LIST_REL (=) = (=)

⊦ option.OPTREL (=) = (=)

⊦ quotient.QUOTIENT (=) id id

⊦ ∀R. quotient_pred_set.FINITER R pred_set.EMPTY

⊦ quotient.--> id id = id

⊦ pair.## id id = id

⊦ quotient.===> (=) (=) = (=)

⊦ quotient_pair.### (=) (=) = (=)

⊦ quotient_sum.+++ (=) (=) = (=)

⊦ ∀P. quotient.?!! P ⇔ (∃!) P

⊦ ∀R. quotient.EQUIV R ⇒ quotient.PARTIAL_EQUIV R

⊦ ∀R. quotient.EQUIV R ⇒ quotient.EQUIV (list.LIST_REL R)

⊦ ∀R. quotient.EQUIV R ⇒ quotient.EQUIV (option.OPTREL R)

⊦ ∀P Q. (P ⇔ Q) ⇒ P ⇒ Q

⊦ ∀R x. quotient.respects R x ⇔ R x x

⊦ ∀R x. bool.IN x (quotient.respects R) ⇔ R x x

⊦ ∀R P.
bool.RES_EXISTS_UNIQUE (quotient.respects R) P ⇒
quotient.RES_EXISTS_EQUIV R P

⊦ ∀P Q. (Q ⇒ P) ⇒ ¬P ⇒ ¬Q

⊦ ∀f g. quotient.--> f g = λh x. g (h (f x))

⊦ ∀E P.
quotient.EQUIV E ⇒ (bool.RES_EXISTS (quotient.respects E) P ⇔ (∃) P)

⊦ ∀E P.
quotient.EQUIV E ⇒
(bool.RES_EXISTS_UNIQUE (quotient.respects E) P ⇔ (∃!) P)

⊦ ∀E P.
quotient.EQUIV E ⇒ (bool.RES_FORALL (quotient.respects E) P ⇔ (∀) P)

⊦ ∀R₁ R₂.
quotient.EQUIV R₁ ⇒ quotient.EQUIV R₂ ⇒
quotient.EQUIV (quotient_pair.### R₁ R₂)

⊦ ∀R₁ R₂.
quotient.EQUIV R₁ ⇒ quotient.EQUIV R₂ ⇒
quotient.EQUIV (quotient_sum.+++ R₁ R₂)

⊦ ∀R abs rep. quotient.QUOTIENT R abs rep ⇒ list.LIST_REL R [] []

⊦ ∀R abs rep. quotient.QUOTIENT R abs rep ⇒ option.OPTREL R none none

⊦ ∀R abs rep. quotient.QUOTIENT R abs rep ⇒ [] = map abs []

⊦ ∀R abs rep. quotient.QUOTIENT R abs rep ⇒ none = map abs none

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
quotient.===> R (⇔) pred_set.EMPTY pred_set.EMPTY

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
quotient.===> R (⇔) pred_set.UNIV pred_set.UNIV

⊦ ∀f s x. bool.IN x (quotient.--> f id s) ⇔ bool.IN (f x) s

⊦ ∀P Q. (∀x. P x ⇒ Q x) ⇒ (∀) P ⇒ (∀) Q

⊦ ∀P Q. (∀x. P x ⇒ Q x) ⇒ (∃) P ⇒ (∃) Q

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
pred_set.EMPTY = quotient.--> rep id pred_set.EMPTY

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
pred_set.UNIV = quotient.--> rep id pred_set.UNIV

⊦ ∀f g h x. quotient.--> f g h x = g (h (f x))

⊦ ∀R abs rep. quotient.QUOTIENT R abs rep ⇒ ∀a. R (rep a) (rep a)

⊦ ∀R abs rep. quotient.QUOTIENT R abs rep ⇒ ∀a. abs (rep a) = a

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
quotient.QUOTIENT (list.LIST_REL R) (map abs) (map rep)

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
quotient.QUOTIENT (option.OPTREL R) (map abs) (map rep)

⊦ ∀E. quotient.EQUIV E ⇔ ∀x y. E x y ⇔ E x = E y

⊦ ∀r lam v.
bool.IN v r ⇒ bool.LET (bool.RES_ABSTRACT r lam) v = bool.LET lam v

⊦ ∀R s₁ s₂.
quotient.===> R (⇔) s₁ s₂ ⇒
(quotient_pred_set.FINITER R s₁ ⇔ quotient_pred_set.FINITER R s₂)

⊦ ∀f g s x. bool.IN x (quotient.--> f g s) ⇔ g (bool.IN (f x) s)

⊦ ∀R abs rep. quotient.QUOTIENT R abs rep ⇒ ∀e. id e = abs (id (rep e))

⊦ ∀R abs rep. quotient.QUOTIENT R abs rep ⇒ ∀l. null l ⇔ null (map rep l)

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒ ∀l. length l = length (map rep l)

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒ ∀x. isNone x ⇔ isNone (map rep x)

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒ ∀x. isSome x ⇔ isSome (map rep x)

⊦ ∀R₁ R₂.
quotient_pair.### R₁ R₂ =
pair.UNCURRY (λa b. pair.UNCURRY (λc d. R₁ a c ∧ R₂ b d))

⊦ ∀R P Q.
    quotient.===> R (⇔) P Q ⇒
    bool.RES_EXISTS_UNIQUE (quotient.respects R) P ⇒
    quotient.RES_EXISTS_EQUIV R Q

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒ ∀x. some x = map abs (some (rep x))

⊦ ∀R abs rep. quotient.QUOTIENT R abs rep ⇒ ∀x y. R x y ⇒ R y x

⊦ ∀R. quotient.EQUIV R ⇒ R a₁ a₂ ∧ R b₁ b₂ ⇒ a₁ = b₁ ⇒ R a₂ b₂

⊦ ∀R x s y.
bool.IN y (quotient_pred_set.INSERTR R x s) ⇔ R y x ∨ bool.IN y s

⊦ ∀R x s.
quotient_pred_set.INSERTR R x s =
pred_set.GSPEC (λy. (y, R y x ∨ bool.IN y s))

⊦ ∀R abs rep. quotient.QUOTIENT R abs rep ⇒ ∀r. R r r ⇒ R (rep (abs r)) r

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
∀l. reverse l = map abs (reverse (map rep l))

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
∀f. (∃!) f ⇔ quotient.RES_EXISTS_EQUIV R (quotient.--> abs id f)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀s.
      pred_set.FINITE s ⇔
      quotient_pred_set.FINITER R (quotient.--> abs id s)

⊦ ∀R s t.
quotient_pred_set.SUBSETR R s t ⇔
bool.RES_FORALL (quotient.respects R) (λx. bool.IN x s ⇒ bool.IN x t)

⊦ ∀x x₁ x₂ x₃.
quotient_sum.+++ x x₁ x₂ x₃ ⇔
quotient_sum.SUM_REL_tupled (x, x₁, x₂, x₃)

⊦ ∀R. (∀x y. R x y ⇔ R x = R y) ⇒ ∀x. list.LIST_REL R x x

⊦ ∀R s t.
quotient_pred_set.PSUBSETR R s t ⇔
quotient_pred_set.SUBSETR R s t ∧ ¬quotient.===> R (⇔) s t

⊦ ∀R.
    bool.RES_FORALL (quotient.respects (quotient.===> R (⇔)))
      (λs.
         quotient_pred_set.FINITER R s ⇒
         bool.RES_FORALL (quotient.respects R)
           (λx.
              quotient_pred_set.FINITER R
                (quotient_pred_set.INSERTR R x s)))

⊦ ∀P P' Q Q'. P = Q ∧ P' = Q' ⇒ P = P' ⇒ Q = Q'

⊦ ∀P P' Q Q'. (P ⇒ Q) ∧ (P' ⇒ Q') ⇒ P ∧ P' ⇒ Q ∧ Q'

⊦ ∀P P' Q Q'. (P ⇒ Q) ∧ (P' ⇒ Q') ⇒ P ∨ P' ⇒ Q ∨ Q'

⊦ ∀P P' Q Q'. (Q ⇒ P) ∧ (P' ⇒ Q') ⇒ (P ⇒ P') ⇒ Q ⇒ Q'

⊦ ∀P R Q. (∀x. R x ∧ (P x ⇒ Q x)) ⇒ (∃) P ⇒ bool.RES_EXISTS R Q

⊦ ∀P R Q. (∀x. R x ∧ (Q x ⇒ P x)) ⇒ bool.RES_FORALL R Q ⇒ (∀) P

⊦ ∀P R Q. (∀x. R x ⇒ P x ⇒ Q x) ⇒ (∀) P ⇒ bool.RES_FORALL R Q

⊦ ∀P R Q. (∀x. R x ⇒ Q x ⇒ P x) ⇒ bool.RES_EXISTS R Q ⇒ (∃) P

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀f.
      (∀) f ⇔ bool.RES_FORALL (quotient.respects R) (quotient.--> abs id f)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀f.
      (∃) f ⇔ bool.RES_EXISTS (quotient.respects R) (quotient.--> abs id f)

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
∀l. concat l = map abs (concat (map (map rep) l))

⊦ ∀R s x y.
bool.IN y (quotient_pred_set.DELETER R s x) ⇔ bool.IN y s ∧ ¬R x y

⊦ ∀R s x.
quotient_pred_set.DELETER R s x =
pred_set.GSPEC (λy. (y, bool.IN y s ∧ ¬R x y))

⊦ ∀R s t.
quotient_pred_set.DISJOINTR R s t ⇔
¬bool.RES_EXISTS (quotient.respects R) (λx. bool.IN x s ∧ bool.IN x t)

⊦ ∀REL abs rep.
quotient.QUOTIENT REL abs rep ⇒
∀x₁ x₂. REL x₁ x₂ ⇒ REL x₁ (rep (abs x₂))

⊦ ∀R abs rep. quotient.QUOTIENT R abs rep ⇒ ∀r s. R r s ⇒ abs r = abs s

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒ ∀e₁ e₂. R e₁ e₂ ⇒ R (id e₁) (id e₂)

⊦ ∀R abs rep. quotient.QUOTIENT R abs rep ⇒ ∀x y. x = y ⇔ R (rep x) (rep y)

⊦ ∀R abs rep. quotient.QUOTIENT R abs rep ⇒ ∀a b. R (rep a) (rep b) ⇔ a = b

⊦ ∀P Q R. (∀x. R x ⇒ P x ⇒ Q x) ⇒ bool.RES_EXISTS R P ⇒ bool.RES_EXISTS R Q

⊦ ∀P Q R. (∀x. R x ⇒ P x ⇒ Q x) ⇒ bool.RES_FORALL R P ⇒ bool.RES_FORALL R Q

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
∀x y. R x y ⇒ option.OPTREL R (some x) (some y)

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
∀l₁ l₂. list.LIST_REL R l₁ l₂ ⇒ (null l₁ ⇔ null l₂)

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
∀l₁ l₂. list.LIST_REL R l₁ l₂ ⇒ length l₁ = length l₂

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
∀x y. option.OPTREL R x y ⇒ (isNone x ⇔ isNone y)

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
∀x y. option.OPTREL R x y ⇒ (isSome x ⇔ isSome y)

⊦ ∀R₁ R₂ f x y.
quotient.respects (quotient.===> R₁ R₂) f ∧ R₁ x y ⇒ R₂ (f x) (f y)

⊦ ∀R₁ R₂ f.
quotient.respects (quotient.===> R₁ R₂) f ⇔
∀x y. R₁ x y ⇒ R₂ (f x) (f y)

⊦ ∀R.
    bool.RES_FORALL (quotient.respects R)
      (λx.
         bool.RES_FORALL (quotient.respects (quotient.===> R (⇔)))
           (λs.
              bool.IN x s ⇔
              quotient.===> R (⇔) (quotient_pred_set.INSERTR R x s) s))

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
∀x s. bool.IN x s ⇔ bool.IN (rep x) (quotient.--> abs id s)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀l₁ l₂.
      list.LIST_REL R l₁ l₂ ⇒ list.LIST_REL R (reverse l₁) (reverse l₂)

⊦ ∀R₁ R₂ f v.
    quotient_pred_set.GSPECR R₁ R₂ f v ⇔
    bool.RES_EXISTS (quotient.respects R₁)
      (λx. quotient_pair.### R₂ (⇔) (v, ⊤) (f x))

⊦ ∀R₁ R₂ f g. quotient.===> R₁ R₂ f g ⇔ ∀x y. R₁ x y ⇒ R₂ (f x) (g y)

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
∀t h. h :: t = map abs (rep h :: map rep t)

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
∀l P. all P l ⇔ all (quotient.--> abs id P) (map rep l)

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
∀l P. any P l ⇔ any (quotient.--> abs id P) (map rep l)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀l₁ l₂.
      list.LIST_REL (list.LIST_REL R) l₁ l₂ ⇒
      list.LIST_REL R (concat l₁) (concat l₂)

⊦ ∀R s t.
quotient.===> R (⇔) s t ⇔ ∀x y. R x y ⇒ (bool.IN x s ⇔ bool.IN y t)

⊦ ∀R₁ R₂ f v.
    bool.IN v (quotient_pred_set.GSPECR R₁ R₂ f) ⇔
    bool.RES_EXISTS (quotient.respects R₁)
      (λx. quotient_pair.### R₂ (⇔) (v, ⊤) (f x))

⊦ ∀R abs rep. quotient.QUOTIENT R abs rep ⇒ ∀x y z. R x y ∧ R y z ⇒ R x z

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
∀l m. l @ m = map abs (map rep l @ map rep m)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀f g.
      quotient.===> R (⇔) f g ⇒
      (quotient.RES_EXISTS_EQUIV R f ⇔ quotient.RES_EXISTS_EQUIV R g)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀s₁ s₂.
      quotient.===> R (⇔) s₁ s₂ ⇒
      (quotient_pred_set.FINITER R s₁ ⇔ quotient_pred_set.FINITER R s₂)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀P f.
      bool.RES_EXISTS P f ⇔
      bool.RES_EXISTS (quotient.--> abs id P) (quotient.--> abs id f)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀P f.
      bool.RES_FORALL P f ⇔
      bool.RES_FORALL (quotient.--> abs id P) (quotient.--> abs id f)

⊦ quotient.RES_EXISTS_EQUIV =
  λR P.
    bool.RES_EXISTS (quotient.respects R) (λx. P x) ∧
    bool.RES_FORALL (quotient.respects R)
      (λx. bool.RES_FORALL (quotient.respects R) (λy. P x ∧ P y ⇒ R x y))

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
∀a b c. (if a then b else c) = abs (if a then rep b else rep c)

⊦ ∀R₁ R₂ a b c d. quotient_pair.### R₁ R₂ (a, b) (c, d) ⇔ R₁ a c ∧ R₂ b d

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
∀P l. filter P l = map abs (filter (quotient.--> abs id P) (map rep l))

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀s t.
      pred_set.DISJOINT s t ⇔
      quotient_pred_set.DISJOINTR R (quotient.--> abs id s)
        (quotient.--> abs id t)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀s t.
      pred_set.PSUBSET s t ⇔
      quotient_pred_set.PSUBSETR R (quotient.--> abs id s)
        (quotient.--> abs id t)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀s t.
      pred_set.SUBSET s t ⇔
      quotient_pred_set.SUBSETR R (quotient.--> abs id s)
        (quotient.--> abs id t)

⊦ ∀R₁ R₂ R₃ f g.
    quotient.respects (quotient.===> R₂ R₃) f ∧
    quotient.respects (quotient.===> R₁ R₂) g ⇒
    quotient.respects (quotient.===> R₁ R₃) (f ∘ g)

⊦ ∀R₁ R₂ y f s.
bool.IN y (quotient_pred_set.IMAGER R₁ R₂ f s) ⇔
bool.RES_EXISTS (quotient.respects R₁) (λx. R₂ y (f x) ∧ bool.IN x s)

⊦ ∀R₁ R₂ f₁ f₂ x₁ x₂.
R₂ (f₁ x₁) (f₂ x₂) ∧ R₁ x₁ x₁ ⇒
R₂ (bool.RES_ABSTRACT (quotient.respects R₁) f₁ x₁) (f₂ x₂)

⊦ ∀R₁ R₂ f₁ f₂ x₁ x₂.
R₂ (f₁ x₁) (f₂ x₂) ∧ R₁ x₂ x₂ ⇒
R₂ (f₁ x₁) (bool.RES_ABSTRACT (quotient.respects R₁) f₂ x₂)

⊦ ∀R₁ R₂ f s.
    quotient_pred_set.IMAGER R₁ R₂ f s =
    pred_set.GSPEC
      (λy.
         (y,
          bool.RES_EXISTS (quotient.respects R₁)
            (λx. R₂ y (f x) ∧ bool.IN x s)))

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀f g.
      quotient.===> R (⇔) f g ⇒
      (bool.RES_EXISTS (quotient.respects R) f ⇔
       bool.RES_EXISTS (quotient.respects R) g)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀f g.
      quotient.===> R (⇔) f g ⇒
      (bool.RES_FORALL (quotient.respects R) f ⇔
       bool.RES_FORALL (quotient.respects R) g)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀s x.
      pred_set.DELETE s x =
      quotient.--> rep id
        (quotient_pred_set.DELETER R (quotient.--> abs id s) (rep x))

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀s x.
      pred_set.INSERT x s =
      quotient.--> rep id
        (quotient_pred_set.INSERTR R (rep x) (quotient.--> abs id s))

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ f g.
      quotient.===> R₁ R₂ f g ⇒
      quotient.===> R₁ R₂ f (bool.RES_ABSTRACT (quotient.respects R₁) g)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ f g.
      quotient.===> R₁ R₂ f g ⇒
      quotient.===> R₁ R₂ (bool.RES_ABSTRACT (quotient.respects R₁) f) g

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀s t.
      pred_set.DIFF s t =
      quotient.--> rep id
        (pred_set.DIFF (quotient.--> abs id s) (quotient.--> abs id t))

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀s t.
      pred_set.INTER s t =
      quotient.--> rep id
        (pred_set.INTER (quotient.--> abs id s) (quotient.--> abs id t))

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀s t.
      pred_set.UNION s t =
      quotient.--> rep id
        (pred_set.UNION (quotient.--> abs id s) (quotient.--> abs id t))

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀a. Data.Sum.isLeft a ⇔ Data.Sum.isLeft (sum.++ rep₁ rep₂ a)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀a. Data.Sum.isRight a ⇔ Data.Sum.isRight (sum.++ rep₁ rep₂ a)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      quotient.QUOTIENT (quotient.===> R₁ R₂) (quotient.--> rep₁ abs₂)
        (quotient.--> abs₁ rep₂)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      quotient.QUOTIENT (quotient_pair.### R₁ R₂) (pair.## abs₁ abs₂)
        (pair.## rep₁ rep₂)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      quotient.QUOTIENT (quotient_sum.+++ R₁ R₂) (sum.++ abs₁ abs₂)
        (sum.++ rep₁ rep₂)

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
∀r s. R r s ⇔ R r r ∧ R s s ∧ abs r = abs s

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
∀r s. R r r ⇒ R s s ⇒ (R r s ⇔ abs r = abs s)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀a. Data.Sum.left a = sum.++ abs₁ abs₂ (Data.Sum.left (rep₁ a))

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀b. Data.Sum.right b = sum.++ abs₁ abs₂ (Data.Sum.right (rep₂ b))

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀p. fst p = abs₁ (fst (pair.## rep₁ rep₂ p))

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀p. snd p = abs₂ (snd (pair.## rep₁ rep₂ p))

⊦ ∀R m.
    quotient.RES_EXISTS_EQUIV R m ⇔
    bool.RES_EXISTS (quotient.respects R) (λx. m x) ∧
    bool.RES_FORALL (quotient.respects R)
      (λx. bool.RES_FORALL (quotient.respects R) (λy. m x ∧ m y ⇒ R x y))

⊦ ∀R.
quotient.PARTIAL_EQUIV R ⇔
(∃x. R x x) ∧ ∀x y. R x y ⇔ R x x ∧ R y y ∧ R x = R y

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
∀x₁ x₂ y₁ y₂. R x₁ x₂ ∧ R y₁ y₂ ⇒ (R x₁ y₁ ⇔ R x₂ y₂)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ f x.
      quotient.respects (quotient.===> R₁ R₂) f ∧ R₁ x x ⇒
      R₂ (f (rep₁ (abs₁ x))) (f x)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀f. (λx. f x) = quotient.--> rep₁ abs₂ (λx. rep₂ (f (abs₁ x)))

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀x y. const x y = abs₁ (const (rep₁ x) (rep₂ y))

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀f x. f x = abs₂ (quotient.--> abs₁ rep₂ f (rep₁ x))

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀x₁ x₂ s₁ s₂.
      R x₁ x₂ ∧ quotient.===> R (⇔) s₁ s₂ ⇒ (bool.IN x₁ s₁ ⇔ bool.IN x₂ s₂)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀t₁ t₂ h₁ h₂.
      R h₁ h₂ ∧ list.LIST_REL R t₁ t₂ ⇒
      list.LIST_REL R (h₁ :: t₁) (h₂ :: t₂)

⊦ ∀R abs rep.
quotient.QUOTIENT R abs rep ⇒
∀s t x y. quotient.===> R (⇔) s t ∧ R x y ⇒ (bool.IN x s ⇔ bool.IN y t)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀f.
        f =
        quotient.--> rep₁ abs₂
          (bool.RES_ABSTRACT (quotient.respects R₁)
             (quotient.--> abs₁ rep₂ f))

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀f.
        (λx. f x) = quotient.--> rep₁ abs₂ (λx. quotient.--> abs₁ rep₂ f x)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀a₁ a₂.
        R₁ a₁ a₂ ⇒
        quotient_sum.+++ R₁ R₂ (Data.Sum.left a₁) (Data.Sum.left a₂)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀b₁ b₂.
        R₂ b₁ b₂ ⇒
        quotient_sum.+++ R₁ R₂ (Data.Sum.right b₁) (Data.Sum.right b₂)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀p₁ p₂. quotient_pair.### R₁ R₂ p₁ p₂ ⇒ R₁ (fst p₁) (fst p₂)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀p₁ p₂. quotient_pair.### R₁ R₂ p₁ p₂ ⇒ R₂ (snd p₁) (snd p₂)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀a₁ a₂.
        quotient_sum.+++ R₁ R₂ a₁ a₂ ⇒
        (Data.Sum.isLeft a₁ ⇔ Data.Sum.isLeft a₂)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀a₁ a₂.
        quotient_sum.+++ R₁ R₂ a₁ a₂ ⇒
        (Data.Sum.isRight a₁ ⇔ Data.Sum.isRight a₂)

⊦ (option.OPTREL R none none ⇔ ⊤) ∧ (option.OPTREL R (some x) none ⇔ ⊥) ∧
(option.OPTREL R none (some y) ⇔ ⊥) ∧
(option.OPTREL R (some x) (some y) ⇔ R x y)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀l₁ l₂ m₁ m₂.
      list.LIST_REL R l₁ l₂ ∧ list.LIST_REL R m₁ m₂ ⇒
      list.LIST_REL R (l₁ @ m₁) (l₂ @ m₂)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀l₁ l₂ P₁ P₂.
      quotient.===> R (⇔) P₁ P₂ ∧ list.LIST_REL R l₁ l₂ ⇒
      (all P₁ l₁ ⇔ all P₂ l₂)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀l₁ l₂ P₁ P₂.
      quotient.===> R (⇔) P₁ P₂ ∧ list.LIST_REL R l₁ l₂ ⇒
      (any P₁ l₁ ⇔ any P₂ l₂)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀a b. (a, b) = pair.## abs₁ abs₂ (rep₁ a, rep₂ b)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀f x.
        bool.literal_case f x =
        abs₂ (bool.literal_case (quotient.--> abs₁ rep₂ f) (rep₁ x))

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀f x.
        bool.LET f x = abs₂ (bool.LET (quotient.--> abs₁ rep₂ f) (rep₁ x))

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀r s.
      list.LIST_REL R r s ⇔
      list.LIST_REL R r r ∧ list.LIST_REL R s s ∧ map abs r = map abs s

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀P₁ P₂ l₁ l₂.
      quotient.===> R (⇔) P₁ P₂ ∧ list.LIST_REL R l₁ l₂ ⇒
      list.LIST_REL R (filter P₁ l₁) (filter P₂ l₂)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀f.
        pred_set.GSPEC f =
        quotient.--> rep₂ id
          (quotient_pred_set.GSPECR R₁ R₂
             (quotient.--> abs₁ (pair.## rep₂ id) f))

⊦ ∀R₁ R₂.
(∀x y. R₁ x y ⇔ R₁ x = R₁ y) ∧ (∀x y. R₂ x y ⇔ R₂ x = R₂ y) ⇒
∀x. quotient_pair.### R₁ R₂ x x

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀l f.
        map f l = map abs₂ (map (quotient.--> abs₁ rep₂ f) (map rep₁ l))

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀a f.
        map f a = map abs₂ (map (quotient.--> abs₁ rep₂ f) (map rep₁ a))

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀f₁ f₂.
        quotient.===> R₁ R₂ f₁ f₂ ⇒
        quotient.===> R₁ R₂ (λx. f₁ x) (λy. f₂ y)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀f x.
        Combinator.w f x =
        abs₂
          (Combinator.w (quotient.--> abs₁ (quotient.--> abs₁ rep₂) f)
             (rep₁ x))

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀x₁ x₂ s₁ s₂.
      R x₁ x₂ ∧ quotient.===> R (⇔) s₁ s₂ ⇒
      quotient.===> R (⇔) (quotient_pred_set.INSERTR R x₁ s₁)
        (quotient_pred_set.INSERTR R x₂ s₂)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀s₁ s₂ x₁ x₂.
      quotient.===> R (⇔) s₁ s₂ ∧ R x₁ x₂ ⇒
      quotient.===> R (⇔) (quotient_pred_set.DELETER R s₁ x₁)
        (quotient_pred_set.DELETER R s₂ x₂)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀s₁ s₂ t₁ t₂.
      quotient.===> R (⇔) s₁ s₂ ∧ quotient.===> R (⇔) t₁ t₂ ⇒
      (quotient_pred_set.DISJOINTR R s₁ t₁ ⇔
       quotient_pred_set.DISJOINTR R s₂ t₂)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀s₁ s₂ t₁ t₂.
      quotient.===> R (⇔) s₁ s₂ ∧ quotient.===> R (⇔) t₁ t₂ ⇒
      (quotient_pred_set.PSUBSETR R s₁ t₁ ⇔
       quotient_pred_set.PSUBSETR R s₂ t₂)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀s₁ s₂ t₁ t₂.
      quotient.===> R (⇔) s₁ s₂ ∧ quotient.===> R (⇔) t₁ t₂ ⇒
      (quotient_pred_set.SUBSETR R s₁ t₁ ⇔
       quotient_pred_set.SUBSETR R s₂ t₂)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀s₁ s₂ t₁ t₂.
      quotient.===> R (⇔) s₁ s₂ ∧ quotient.===> R (⇔) t₁ t₂ ⇒
      quotient.===> R (⇔) (pred_set.DIFF s₁ t₁) (pred_set.DIFF s₂ t₂)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀s₁ s₂ t₁ t₂.
      quotient.===> R (⇔) s₁ s₂ ∧ quotient.===> R (⇔) t₁ t₂ ⇒
      quotient.===> R (⇔) (pred_set.INTER s₁ t₁) (pred_set.INTER s₂ t₂)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀s₁ s₂ t₁ t₂.
      quotient.===> R (⇔) s₁ s₂ ∧ quotient.===> R (⇔) t₁ t₂ ⇒
      quotient.===> R (⇔) (pred_set.UNION s₁ t₁) (pred_set.UNION s₂ t₂)

⊦ ∀R s.
    quotient_pred_set.FINITER R s ⇔
    bool.RES_FORALL
      (quotient.respects (quotient.===> (quotient.===> R (⇔)) (⇔)))
      (λP.
         P pred_set.EMPTY ∧
         bool.RES_FORALL (quotient.respects (quotient.===> R (⇔)))
           (λs.
              P s ⇒
              bool.RES_FORALL (quotient.respects R)
                (λe. P (quotient_pred_set.INSERTR R e s))) ⇒ P s)

⊦ quotient_sum.SUM_REL_tupled =
  relation.WFREC (select R. wellFounded R)
    (λSUM_REL_tupled a.
       pair.pair_CASE a
         (λR₁ v₁.
            pair.pair_CASE v₁
              (λR₂ v₃.
                 pair.pair_CASE v₃
                   (λv₄ v₅.
                      sum.sum_CASE v₄
                        (λa₁.
                           sum.sum_CASE v₅ (λa₂. id (R₁ a₁ a₂))
                             (λb2'. id ⊥))
                        (λb₁.
                           sum.sum_CASE v₅ (λa2'. id ⊥)
                             (λb₂. id (R₂ b₁ b₂)))))))

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀f₁ f₂.
        quotient.===> R₁ R₂ f₁ f₂ ⇒
        quotient.===> R₁ R₂ (bool.RES_ABSTRACT (quotient.respects R₁) f₁)
          (bool.RES_ABSTRACT (quotient.respects R₁) f₂)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇒
    ∀a₁ a₂ b₁ b₂ c₁ c₂.
      (a₁ ⇔ a₂) ∧ R b₁ b₂ ∧ R c₁ c₂ ⇒
      R (if a₁ then b₁ else c₁) (if a₂ then b₂ else c₂)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀x₁ x₂ y₁ y₂. R₁ x₁ x₂ ∧ R₂ y₁ y₂ ⇒ R₁ (const x₁ y₁) (const x₂ y₂)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀f g x y. quotient.===> R₁ R₂ f g ∧ R₁ x y ⇒ R₂ (f x) (g y)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀f s.
        pred_set.IMAGE f s =
        quotient.--> rep₂ id
          (quotient_pred_set.IMAGER R₁ R₂ (quotient.--> abs₁ rep₂ f)
             (quotient.--> abs₁ id s))

⊦ ∀P R Q.
    (∀x. P x ⇒ Q x) ∧
    (∀x y.
       quotient.respects R x ∧ Q x ∧ quotient.respects R y ∧ Q y ⇒ R x y) ⇒
    bool.RES_EXISTS_UNIQUE (quotient.respects R) P ⇒
    quotient.RES_EXISTS_EQUIV R Q

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀f₁ f₂.
        quotient.===> R₁ (quotient_pair.### R₂ (⇔)) f₁ f₂ ⇒
        quotient.===> R₂ (⇔) (quotient_pred_set.GSPECR R₁ R₂ f₁)
          (quotient_pred_set.GSPECR R₁ R₂ f₂)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀l f e.
        list.FOLDR f e l =
        abs₂
          (list.FOLDR (quotient.--> abs₁ (quotient.--> abs₂ rep₂) f)
             (rep₂ e) (map rep₁ l))

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀l f e.
        list.FOLDL f e l =
        abs₁
          (list.FOLDL (quotient.--> abs₁ (quotient.--> abs₂ rep₁) f)
             (rep₁ e) (map rep₂ l))

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀a₁ a₂ b₁ b₂.
        R₁ a₁ b₁ ∧ R₂ a₂ b₂ ⇒ quotient_pair.### R₁ R₂ (a₁, a₂) (b₁, b₂)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀f g x y.
        quotient.===> R₁ R₂ f g ∧ R₁ x y ⇒
        R₂ (bool.literal_case f x) (bool.literal_case g y)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀f g x y.
        quotient.===> R₁ R₂ f g ∧ R₁ x y ⇒ R₂ (bool.LET f x) (bool.LET g y)

⊦ ∀P E Q.
    (∀x. P x ⇒ quotient.respects E x ∧ Q x) ∧
    (∀x y.
       quotient.respects E x ∧ Q x ∧ quotient.respects E y ∧ Q y ⇒ E x y) ⇒
    (∃!) P ⇒ quotient.RES_EXISTS_EQUIV E Q

⊦ (quotient_sum.+++ R₁ R₂ (Data.Sum.left a₁) (Data.Sum.left a₂) ⇔
   R₁ a₁ a₂) ∧
  (quotient_sum.+++ R₁ R₂ (Data.Sum.right b₁) (Data.Sum.right b₂) ⇔
   R₂ b₁ b₂) ∧
  (quotient_sum.+++ R₁ R₂ (Data.Sum.left a₁) (Data.Sum.right b₂) ⇔ ⊥) ∧
  (quotient_sum.+++ R₁ R₂ (Data.Sum.right b₁) (Data.Sum.left a₂) ⇔ ⊥)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀l₁ l₂ f₁ f₂.
        quotient.===> R₁ R₂ f₁ f₂ ∧ list.LIST_REL R₁ l₁ l₂ ⇒
        list.LIST_REL R₂ (map f₁ l₁) (map f₂ l₂)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀a₁ a₂ f₁ f₂.
        quotient.===> R₁ R₂ f₁ f₂ ∧ option.OPTREL R₁ a₁ a₂ ⇒
        option.OPTREL R₂ (map f₁ a₁) (map f₂ a₂)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀f₁ f₂ x₁ x₂.
        quotient.===> R₁ (quotient.===> R₁ R₂) f₁ f₂ ∧ R₁ x₁ x₂ ⇒
        R₂ (Combinator.w f₁ x₁) (Combinator.w f₂ x₂)

⊦ ∀R abs rep.
    quotient.QUOTIENT R abs rep ⇔
    (∀a. abs (rep a) = a) ∧ (∀a. R (rep a) (rep a)) ∧
    ∀r s. R r s ⇔ R r r ∧ R s s ∧ abs r = abs s

⊦ ∀R.
(∀x y. R x y ⇔ R x = R y) ⇔
(∀x. R x x) ∧ (∀x y. R x y ⇒ R y x) ∧ ∀x y z. R x y ∧ R y z ⇒ R x z

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀R₃ abs₃ rep₃.
        quotient.QUOTIENT R₃ abs₃ rep₃ ⇒
        ∀f g.
          f ∘ g =
          quotient.--> rep₁ abs₃
            (quotient.--> abs₂ rep₃ f ∘ quotient.--> abs₁ rep₂ g)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀R₃ abs₃ rep₃.
        quotient.QUOTIENT R₃ abs₃ rep₃ ⇒
        ∀f p.
          pair.UNCURRY f p =
          abs₃
            (pair.UNCURRY (quotient.--> abs₁ (quotient.--> abs₂ rep₃) f)
               (pair.## rep₁ rep₂ p))

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀R₃ abs₃ rep₃.
        quotient.QUOTIENT R₃ abs₃ rep₃ ⇒
        ∀f₁ f₂.
          quotient.===> R₁ (quotient.===> R₂ R₃) f₁ f₂ ⇒
          quotient.===> (quotient_pair.### R₁ R₂) R₃ (pair.UNCURRY f₁)
            (pair.UNCURRY f₂)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀R₃ abs₃ rep₃.
        quotient.QUOTIENT R₃ abs₃ rep₃ ⇒
        ∀f₁ f₂.
          quotient.===> (quotient_pair.### R₁ R₂) R₃ f₁ f₂ ⇒
          quotient.===> R₁ (quotient.===> R₂ R₃) (pair.CURRY f₁)
            (pair.CURRY f₂)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀f g.
        quotient.===> R₁ R₂ f g ⇔
        quotient.respects (quotient.===> R₁ R₂) f ∧
        quotient.respects (quotient.===> R₁ R₂) g ∧
        quotient.--> rep₁ abs₂ f = quotient.--> rep₁ abs₂ g

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀f₁ f₂ s₁ s₂.
        quotient.===> R₁ R₂ f₁ f₂ ∧ quotient.===> R₁ (⇔) s₁ s₂ ⇒
        quotient.===> R₂ (⇔) (quotient_pred_set.IMAGER R₁ R₂ f₁ s₁)
          (quotient_pred_set.IMAGER R₁ R₂ f₂ s₂)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀R₃ abs₃ rep₃.
        quotient.QUOTIENT R₃ abs₃ rep₃ ⇒
        ∀f x y.
          flip f x y =
          abs₃
            (flip (quotient.--> abs₁ (quotient.--> abs₂ rep₃) f) (rep₂ x)
               (rep₁ y))

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀R₃ abs₃ rep₃.
        quotient.QUOTIENT R₃ abs₃ rep₃ ⇒
        ∀f a b.
          pair.CURRY f a b =
          abs₃
            (pair.CURRY (quotient.--> (pair.## abs₁ abs₂) rep₃ f) (rep₁ a)
               (rep₂ b))

⊦ ∀R.
    bool.RES_FORALL
      (quotient.respects (quotient.===> (quotient.===> R (⇔)) (⇔)))
      (λP.
         P pred_set.EMPTY ∧
         bool.RES_FORALL (quotient.respects (quotient.===> R (⇔)))
           (λs.
              quotient_pred_set.FINITER R s ∧ P s ⇒
              bool.RES_FORALL (quotient.respects R)
                (λe. ¬bool.IN e s ⇒ P (quotient_pred_set.INSERTR R e s))) ⇒
         bool.RES_FORALL (quotient.respects (quotient.===> R (⇔)))
           (λs. quotient_pred_set.FINITER R s ⇒ P s))

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀l₁ l₂ f₁ f₂ e₁ e₂.
        quotient.===> R₁ (quotient.===> R₂ R₂) f₁ f₂ ∧ R₂ e₁ e₂ ∧
        list.LIST_REL R₁ l₁ l₂ ⇒
        R₂ (list.FOLDR f₁ e₁ l₁) (list.FOLDR f₂ e₂ l₂)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀l₁ l₂ f₁ f₂ e₁ e₂.
        quotient.===> R₁ (quotient.===> R₂ R₁) f₁ f₂ ∧ R₁ e₁ e₂ ∧
        list.LIST_REL R₂ l₁ l₂ ⇒
        R₁ (list.FOLDL f₁ e₁ l₁) (list.FOLDL f₂ e₂ l₂)

⊦ ∀REL₁ abs₁ rep₁ REL₂ abs₂ rep₂ f₁ f₂.
    ((∀r r'. REL₁ r r' ⇒ REL₁ r (rep₁ (abs₁ r'))) ∧
     ∀r r'. REL₂ r r' ⇒ REL₂ r (rep₂ (abs₂ r'))) ∧
    quotient.===> REL₁ REL₂ f₁ f₂ ⇒
    quotient.===> REL₁ REL₂ f₁
      (quotient.--> abs₁ rep₂ (quotient.--> rep₁ abs₂ f₂))

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀R₃ abs₃ rep₃.
        quotient.QUOTIENT R₃ abs₃ rep₃ ⇒
        ∀f₁ f₂ g₁ g₂.
          quotient.===> R₂ R₃ f₁ f₂ ∧ quotient.===> R₁ R₂ g₁ g₂ ⇒
          quotient.===> R₁ R₃ (f₁ ∘ g₁) (f₂ ∘ g₂)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀f g.
        quotient.respects (quotient.===> R₁ R₂) f ∧
        quotient.respects (quotient.===> R₁ R₂) g ⇒
        (quotient.--> rep₁ abs₂ f = quotient.--> rep₁ abs₂ g ⇔
         ∀x y. R₁ x y ⇒ R₂ (f x) (g y))

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀f g.
        quotient.respects (quotient.===> R₁ R₂) f ∧
        quotient.respects (quotient.===> R₁ R₂) g ∧
        quotient.--> rep₁ abs₂ f = quotient.--> rep₁ abs₂ g ⇒
        ∀x y. R₁ x y ⇒ R₂ (f x) (g y)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀R₃ abs₃ rep₃.
        quotient.QUOTIENT R₃ abs₃ rep₃ ⇒
        ∀R₄ abs₄ rep₄.
          quotient.QUOTIENT R₄ abs₄ rep₄ ⇒
          ∀f g.
            pair.## f g =
            quotient.--> (pair.## rep₁ rep₃) (pair.## abs₂ abs₄)
              (pair.## (quotient.--> abs₁ rep₂ f)
                 (quotient.--> abs₃ rep₄ g))

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀R₃ abs₃ rep₃.
        quotient.QUOTIENT R₃ abs₃ rep₃ ⇒
        ∀R₄ abs₄ rep₄.
          quotient.QUOTIENT R₄ abs₄ rep₄ ⇒
          ∀f g.
            sum.++ f g =
            quotient.--> (sum.++ rep₁ rep₃) (sum.++ abs₂ abs₄)
              (sum.++ (quotient.--> abs₁ rep₂ f)
                 (quotient.--> abs₃ rep₄ g))

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀R₃ abs₃ rep₃.
        quotient.QUOTIENT R₃ abs₃ rep₃ ⇒
        ∀f₁ f₂ x₁ x₂ y₁ y₂.
          quotient.===> R₁ (quotient.===> R₂ R₃) f₁ f₂ ∧ R₂ x₁ x₂ ∧
          R₁ y₁ y₂ ⇒ R₃ (flip f₁ x₁ y₁) (flip f₂ x₂ y₂)

⊦ ∀P.
    (∀R₁ R₂ a₁ a₂. P R₁ R₂ (Data.Sum.left a₁) (Data.Sum.left a₂)) ∧
    (∀R₁ R₂ b₁ b₂. P R₁ R₂ (Data.Sum.right b₁) (Data.Sum.right b₂)) ∧
    (∀R₁ R₂ a₁ b₂. P R₁ R₂ (Data.Sum.left a₁) (Data.Sum.right b₂)) ∧
    (∀R₁ R₂ b₁ a₂. P R₁ R₂ (Data.Sum.right b₁) (Data.Sum.left a₂)) ⇒
    ∀v v₁ v₂ v₃. P v v₁ v₂ v₃

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀R₃ abs₃ rep₃.
        quotient.QUOTIENT R₃ abs₃ rep₃ ⇒
        ∀R₄ abs₄ rep₄.
          quotient.QUOTIENT R₄ abs₄ rep₄ ⇒
          ∀f₁ f₂ g₁ g₂.
            quotient.===> R₁ R₂ f₁ f₂ ∧ quotient.===> R₃ R₄ g₁ g₂ ⇒
            quotient.===> (quotient_pair.### R₁ R₃)
              (quotient_pair.### R₂ R₄) (pair.## f₁ g₁) (pair.## f₂ g₂)

⊦ ∀R₁ abs₁ rep₁.
    quotient.QUOTIENT R₁ abs₁ rep₁ ⇒
    ∀R₂ abs₂ rep₂.
      quotient.QUOTIENT R₂ abs₂ rep₂ ⇒
      ∀R₃ abs₃ rep₃.
        quotient.QUOTIENT R₃ abs₃ rep₃ ⇒
        ∀R₄ abs₄ rep₄.
          quotient.QUOTIENT R₄ abs₄ rep₄ ⇒
          ∀f₁ f₂ g₁ g₂.
            quotient.===> R₁ R₂ f₁ f₂ ∧ quotient.===> R₃ R₄ g₁ g₂ ⇒
            quotient.===> (quotient_sum.+++ R₁ R₃) (quotient_sum.+++ R₂ R₄)
              (sum.++ f₁ g₁) (sum.++ f₂ g₂)

External Type Operators

→
bool
Data
- List
  - list
- Option
  - option
- Pair
  - ×
- Sum
  - Data.Sum.+
Number
- Natural
  - natural

External Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∃!
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
- List
  - ::
  - @
  - []
  - all
  - any
  - concat
  - filter
  - length
  - map
  - null
  - reverse
- Option
  - isNone
  - isSome
  - map
  - none
  - some
- Pair
  - ,
  - fst
  - snd
- Sum
  - Data.Sum.isLeft
  - Data.Sum.isRight
  - Data.Sum.left
  - Data.Sum.right
Function
- const
- flip
- id
- ∘
- Combinator
  - Combinator.w
HOL4
- bool
  - bool.literal_case
  - bool.IN
  - bool.LET
  - bool.RES_ABSTRACT
  - bool.RES_EXISTS
  - bool.RES_EXISTS_UNIQUE
  - bool.RES_FORALL
- list
  - list.FOLDL
  - list.FOLDR
  - list.LIST_REL
- option
  - option.option_CASE
  - option.OPTION_JOIN
  - option.OPTREL
  - option.THE
- pair
  - pair.##
  - pair.pair_CASE
  - pair.CURRY
  - pair.UNCURRY
- pred_set
  - pred_set.DELETE
  - pred_set.DIFF
  - pred_set.DISJOINT
  - pred_set.EMPTY
  - pred_set.FINITE
  - pred_set.GSPEC
  - pred_set.IMAGE
  - pred_set.INSERT
  - pred_set.INTER
  - pred_set.PSUBSET
  - pred_set.SUBSET
  - pred_set.UNION
  - pred_set.UNIV
- relation
  - relation.RESTRICT
  - relation.WFREC
- sum
  - sum.++
  - sum.sum_CASE
Number
- Natural
  - suc
  - zero
Relation
- empty
- wellFounded

Assumptions

⊦ ⊤

⊦ wellFounded empty

⊦ ∀x. bool.IN x pred_set.UNIV

⊦ ∀t. ⊥ ⇒ t

⊦ bool.IN = λx f. f x

⊦ bool.literal_case = λf x. f x

⊦ bool.LET = λf x. f x

⊦ ¬¬p ⇒ p

⊦ ∀x. ¬bool.IN x pred_set.EMPTY

⊦ ∀x. id x = x

⊦ ∀t. t ∨ ¬t

⊦ (¬) = λt. t ⇒ ⊥

⊦ (∃) = λP. P ((select) P)

⊦ ∀t. (∀x. t) ⇔ t

⊦ ∀t. (∃x. t) ⇔ t

⊦ ∀t. (λx. t x) = t

⊦ (∀) = λP. P = λx. ⊤

⊦ ¬(p ⇒ q) ⇒ p

⊦ ∀x. x = x ⇔ ⊤

⊦ ∀t. ¬¬t ⇔ t

⊦ ¬(p ⇒ q) ⇒ ¬q

⊦ ¬(p ∨ q) ⇒ ¬p

⊦ ¬(p ∨ q) ⇒ ¬q

⊦ ∀A. A ⇒ ¬A ⇒ ⊥

⊦ ∀t. ¬t ⇒ t ⇒ ⊥

⊦ ∀t. (t ⇒ ⊥) ⇒ ¬t

⊦ ∀x y. const x y = x

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ ∀x. (fst x, snd x) = x

⊦ ∀x y. ¬(Data.Sum.left x = Data.Sum.right y)

⊦ ∀x y. fst (x, y) = x

⊦ ∀x y. snd (x, y) = y

⊦ ∀a₁ a₀. ¬([] = a₀ :: a₁)

⊦ ∀a₁ a₀. ¬(a₀ :: a₁ = [])

⊦ ∀P x. P x ⇒ P ((select) P)

⊦ ∀P x. bool.IN x P ⇔ P x

⊦ pair.pair_CASE (x, y) f = f x y

⊦ ∀x. ∃q r. x = (q, r)

⊦ ∀x y. x = y ⇔ y = x

⊦ ∀x y. x = y ⇒ y = x

⊦ ∀A B. A ∨ B ⇔ B ∨ A

⊦ ∀f x. Combinator.w f x = f x x

⊦ (¬A ⇒ ⊥) ⇒ (A ⇒ ⊥) ⇒ ⊥

⊦ ∀opt. opt = none ∨ ∃x. opt = some x

⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤

⊦ null [] ∧ ∀h t. ¬null (h :: t)

⊦ (∀x. Data.Sum.isLeft (Data.Sum.left x)) ∧
∀y. ¬Data.Sum.isLeft (Data.Sum.right y)

⊦ (∀x. Data.Sum.isRight (Data.Sum.right x)) ∧
∀y. ¬Data.Sum.isRight (Data.Sum.left y)

⊦ ∀P. ¬(∀x. P x) ⇔ ∃x. ¬P x

⊦ ∀P. ¬(∃x. P x) ⇔ ∀x. ¬P x

⊦ (∃) = λP. ∀q. (∀x. P x ⇒ q) ⇒ q

⊦ (∀x. isNone (some x) ⇔ ⊥) ∧ (isNone none ⇔ ⊤)

⊦ (∀x. isSome (some x) ⇔ ⊤) ∧ (isSome none ⇔ ⊥)

⊦ ∀m n. suc m = suc n ⇔ m = n

⊦ ∀s t. pred_set.DISJOINT s t ⇔ pred_set.INTER s t = pred_set.EMPTY

⊦ ∀f g x. (f ∘ g) x = f (g x)

⊦ ∀f x y. flip f x y = f y x

⊦ ∀l. l = [] ∨ ∃h t. l = h :: t

⊦ ∀f g. f = g ⇔ ∀x. f x = g x

⊦ ∀ss. (∃x. ss = Data.Sum.left x) ∨ ∃y. ss = Data.Sum.right y

⊦ ∀f x y. pair.UNCURRY f (x, y) = f x y

⊦ ∀f x y. pair.CURRY f x y = f (x, y)

⊦ (∨) = λt₁ t₂. ∀t. (t₁ ⇒ t) ⇒ (t₂ ⇒ t) ⇒ t

⊦ ∀t₁ t₂. (t₁ ⇒ t₂) ⇒ (t₂ ⇒ t₁) ⇒ (t₁ ⇔ t₂)

⊦ (p ⇔ ¬q) ⇔ (p ∨ q) ∧ (¬q ∨ ¬p)

⊦ ¬(¬A ∨ B) ⇒ ⊥ ⇔ A ⇒ ¬B ⇒ ⊥

⊦ ∀P f. bool.RES_EXISTS P f ⇔ ∃x. bool.IN x P ∧ f x

⊦ ∀P f. bool.RES_FORALL P f ⇔ ∀x. bool.IN x P ⇒ f x

⊦ ∀P Q. (∀y. P ∨ Q y) ⇔ P ∨ ∀x. Q x

⊦ ∀P Q. (∃y. P ∧ Q y) ⇔ P ∧ ∃x. Q x

⊦ ∀P Q. P ∨ (∃x. Q x) ⇔ ∃y. P ∨ Q y

⊦ ∀P Q. (∃x. P x ∧ Q) ⇔ (∃x. P x) ∧ Q

⊦ ∀P Q. (∃x. P x) ∨ Q ⇔ ∃a₂. P a₂ ∨ Q

⊦ ∀s t. pred_set.PSUBSET s t ⇔ pred_set.SUBSET s t ∧ ¬(s = t)

⊦ ¬(A ∨ B) ⇒ ⊥ ⇔ (A ⇒ ⊥) ⇒ ¬B ⇒ ⊥

⊦ (x, y) = (a, b) ⇔ x = a ∧ y = b

⊦ ∀x y z. x = y ∧ y = z ⇒ x = z

⊦ ∀t₁ t₂ t₃. t₁ ∧ t₂ ∧ t₃ ⇔ (t₁ ∧ t₂) ∧ t₃

⊦ ∀t₁ t₂ t₃. t₁ ⇒ t₂ ⇒ t₃ ⇔ t₁ ∧ t₂ ⇒ t₃

⊦ ∀A B C. A ∨ B ∨ C ⇔ (A ∨ B) ∨ C

⊦ ∀p m x. bool.IN x p ⇒ bool.RES_ABSTRACT p m x = m x

⊦ ∀s t. s = t ⇔ ∀x. bool.IN x s ⇔ bool.IN x t

⊦ ∀s t. pred_set.SUBSET s t ⇔ ∀x. bool.IN x s ⇒ bool.IN x t

⊦ ∀f v. bool.IN v (pred_set.GSPEC f) ⇔ ∃x. (v, ⊤) = f x

⊦ ∀t₁ t₂. (if ⊤ then t₁ else t₂) = t₁ ∧ (if ⊥ then t₁ else t₂) = t₂

⊦ length [] = 0 ∧ ∀h t. length (h :: t) = suc (length t)

⊦ ∀f g p. pair.## f g p = (f (fst p), g (snd p))

⊦ (∀t. ¬¬t ⇔ t) ∧ (¬⊤ ⇔ ⊥) ∧ (¬⊥ ⇔ ⊤)

⊦ concat [] = [] ∧ ∀h t. concat (h :: t) = h @ concat t

⊦ ∀x y s. bool.IN x (pred_set.INSERT y s) ⇔ x = y ∨ bool.IN x s

⊦ ∀f l₁ l₂. map f (l₁ @ l₂) = map f l₁ @ map f l₂

⊦ ∀s t x. bool.IN x (pred_set.INTER s t) ⇔ bool.IN x s ∧ bool.IN x t

⊦ ∀s t x. bool.IN x (pred_set.UNION s t) ⇔ bool.IN x s ∨ bool.IN x t

⊦ (∃!) = λP. (∃) P ∧ ∀x y. P x ∧ P y ⇒ x = y

⊦ ∀f b x y. f (if b then x else y) = if b then f x else f y

⊦ ∀f g x y. pair.## f g (x, y) = (f x, g y)

⊦ ∀s x y. bool.IN x (pred_set.DELETE s y) ⇔ bool.IN x s ∧ ¬(x = y)

⊦ ∀s t x. bool.IN x (pred_set.DIFF s t) ⇔ bool.IN x s ∧ ¬bool.IN x t

⊦ ∀P Q. (∀x. P x ∧ Q x) ⇔ (∀x. P x) ∧ ∀x. Q x

⊦ ∀P Q. (∃x. P x ∨ Q x) ⇔ (∃x. P x) ∨ ∃x. Q x

⊦ (∀f x. map f (some x) = some (f x)) ∧ ∀f. map f none = none

⊦ ∀P. P [] ∧ (∀t. P t ⇒ ∀h. P (h :: t)) ⇒ ∀l. P l

⊦ reverse [] = [] ∧ ∀h t. reverse (h :: t) = reverse t @ h :: []

⊦ ∀y s f. bool.IN y (pred_set.IMAGE f s) ⇔ ∃x. y = f x ∧ bool.IN x s

⊦ ∀a₀ a₁ a0' a1'. a₀ :: a₁ = a0' :: a1' ⇔ a₀ = a0' ∧ a₁ = a1'

⊦ ∀s.
pred_set.FINITE s ⇔
∀P. P pred_set.EMPTY ∧ (∀s. P s ⇒ ∀e. P (pred_set.INSERT e s)) ⇒ P s

⊦ (p ⇔ q ⇒ r) ⇔ (p ∨ q) ∧ (p ∨ ¬r) ∧ (¬q ∨ r ∨ ¬p)

⊦ (p ⇔ q ∨ r) ⇔ (p ∨ ¬q) ∧ (p ∨ ¬r) ∧ (q ∨ r ∨ ¬p)

⊦ ∀R. wellFounded R ⇒ ∀P. (∀x. (∀y. R y x ⇒ P y) ⇒ P x) ⇒ ∀x. P x

⊦ (p ⇔ q ∧ r) ⇔ (p ∨ ¬q ∨ ¬r) ∧ (q ∨ ¬p) ∧ (r ∨ ¬p)

⊦ (∀l. [] @ l = l) ∧ ∀l₁ l₂ h. (h :: l₁) @ l₂ = h :: l₁ @ l₂

⊦ ∀A B. (¬(A ∧ B) ⇔ ¬A ∨ ¬B) ∧ (¬(A ∨ B) ⇔ ¬A ∧ ¬B)

⊦ ∀M R f.
f = relation.WFREC R M ⇒ wellFounded R ⇒
∀x. f x = M (relation.RESTRICT f R x) x

⊦ (∀f. map f [] = []) ∧ ∀f h t. map f (h :: t) = f h :: map f t

⊦ (∀P. all P [] ⇔ ⊤) ∧ ∀P h t. all P (h :: t) ⇔ P h ∧ all P t

⊦ (∀P. any P [] ⇔ ⊥) ∧ ∀P h t. any P (h :: t) ⇔ P h ∨ any P t

⊦ (∀y x. Data.Sum.left x = Data.Sum.left y ⇔ x = y) ∧
∀y x. Data.Sum.right x = Data.Sum.right y ⇔ x = y

⊦ (∀x f f₁. sum.sum_CASE (Data.Sum.left x) f f₁ = f x) ∧
∀y f f₁. sum.sum_CASE (Data.Sum.right y) f f₁ = f₁ y

⊦ ∀t. ((⊤ ⇔ t) ⇔ t) ∧ ((t ⇔ ⊤) ⇔ t) ∧ ((⊥ ⇔ t) ⇔ ¬t) ∧ ((t ⇔ ⊥) ⇔ ¬t)

⊦ ∀P f.
    bool.RES_EXISTS_UNIQUE P f ⇔
    bool.RES_EXISTS P (λx. f x) ∧
    bool.RES_FORALL P (λx. bool.RES_FORALL P (λy. f x ∧ f y ⇒ x = y))

⊦ (∀f g a. sum.++ f g (Data.Sum.left a) = Data.Sum.left (f a)) ∧
∀f g b. sum.++ f g (Data.Sum.right b) = Data.Sum.right (g b)

⊦ (∀P. filter P [] = []) ∧
∀P h t. filter P (h :: t) = if P h then h :: filter P t else filter P t

⊦ (∀f e. list.FOLDR f e [] = e) ∧
∀f e x l. list.FOLDR f e (x :: l) = f x (list.FOLDR f e l)

⊦ (∀f e. list.FOLDL f e [] = e) ∧
∀f e x l. list.FOLDL f e (x :: l) = list.FOLDL f (f e x) l

⊦ ∀t. (⊤ ∧ t ⇔ t) ∧ (t ∧ ⊤ ⇔ t) ∧ (⊥ ∧ t ⇔ ⊥) ∧ (t ∧ ⊥ ⇔ ⊥) ∧ (t ∧ t ⇔ t)

⊦ ∀t. (⊤ ∨ t ⇔ ⊤) ∧ (t ∨ ⊤ ⇔ ⊤) ∧ (⊥ ∨ t ⇔ t) ∧ (t ∨ ⊥ ⇔ t) ∧ (t ∨ t ⇔ t)

⊦ ∀t. (⊤ ⇒ t ⇔ t) ∧ (t ⇒ ⊤ ⇔ ⊤) ∧ (⊥ ⇒ t ⇔ ⊤) ∧ (t ⇒ t ⇔ ⊤) ∧ (t ⇒ ⊥ ⇔ ¬t)

⊦ ∀R x y.
option.OPTREL R x y ⇔
x = none ∧ y = none ∨ ∃x₀ y₀. x = some x₀ ∧ y = some y₀ ∧ R x₀ y₀

⊦ (p ⇔ q ⇔ r) ⇔ (p ∨ q ∨ r) ∧ (p ∨ ¬r ∨ ¬q) ∧ (q ∨ ¬r ∨ ¬p) ∧ (r ∨ ¬q ∨ ¬p)

⊦ (list.LIST_REL R [] [] ⇔ ⊤) ∧ (list.LIST_REL R (a :: as) [] ⇔ ⊥) ∧
(list.LIST_REL R [] (b :: bs) ⇔ ⊥) ∧
(list.LIST_REL R (a :: as) (b :: bs) ⇔ R a b ∧ list.LIST_REL R as bs)

⊦ (∀x y. some x = some y ⇔ x = y) ∧ (∀x. option.THE (some x) = x) ∧
  (∀x. ¬(none = some x)) ∧ (∀x. ¬(some x = none)) ∧
  (∀x. isSome (some x) ⇔ ⊤) ∧ (isSome none ⇔ ⊥) ∧
  (∀x. isNone x ⇔ x = none) ∧ (∀x. ¬isSome x ⇔ x = none) ∧
  (∀x. isSome x ⇒ some (option.THE x) = x) ∧
  (∀x. option.option_CASE x none some = x) ∧
  (∀x. option.option_CASE x x some = x) ∧
  (∀x. isNone x ⇒ option.option_CASE x e f = e) ∧
  (∀x. isSome x ⇒ option.option_CASE x e f = f (option.THE x)) ∧
  (∀x. isSome x ⇒ option.option_CASE x e some = x) ∧
  (∀v f. option.option_CASE none v f = v) ∧
  (∀x v f. option.option_CASE (some x) v f = f x) ∧
  (∀f x. map f (some x) = some (f x)) ∧ (∀f. map f none = none) ∧
  option.OPTION_JOIN none = none ∧ ∀x. option.OPTION_JOIN (some x) = x