Theory transfer

⊢ ∀R. bi_unique R ⇔ left_unique R ∧ right_unique R

⊢ ∀R. bitotal R ⇔ total R ∧ surj R

⊢ ∀A. equalityp A ⇔ A = $=

⊢ ∀R. left_unique R ⇔ ∀a1 a2 b. R a1 b ∧ R a2 b ⇒ a1 = a2

⊢ ∀R. right_unique R ⇔ ∀a b1 b2. R a b1 ∧ R a b2 ⇒ b1 = b2

⊢ ∀R. surj R ⇔ ∀y. ∃x. R x y

⊢ ∀R. total R ⇔ ∀x. ∃y. R x y

⊢ left_unique AB ⇒
  right_unique AB ⇒
  (LIST_REL AB |==> $<=>) ALL_DISTINCT ALL_DISTINCT

⊢ bitotal AB ⇒ ((AB |==> $<=>) |==> $<=>) $! $!

⊢ surj AB ⇒ ((AB |==> $<=>) |==> $<=>) (RES_FORALL (RDOM AB)) $!

⊢ surj AB ⇒ ((AB |==> $<=>) |==> $==>) $! $!

⊢ surj AB ⇒ ((AB |==> $==>) |==> $==>) $! $!

⊢ total AB ⇒ ((AB |==> $<=>) |==> $<=>) $! (RES_FORALL (RRANGE AB))

⊢ total AB ⇒ ((AB |==> flip $==>) |==> flip $==>) $! $!

⊢ total AB ⇒ ((AB |==> $<=>) |==> flip $==>) $! $!

⊢ total AB ⇒ ((AB |==> $<=>) |==> $==>) $! (RES_FORALL (RRANGE AB))

⊢ (AB |==> CD |==> AB ### CD) $, $,

⊢ ($<=> |==> AB |==> AB |==> AB) COND COND

⊢ (AB |==> LIST_REL AB |==> LIST_REL AB) CONS CONS

⊢ bi_unique AB ⇒ (AB |==> AB |==> $<=>) $= $=

⊢ surj AB ⇒ ((AB |==> $<=>) |==> $<=>) (RES_EXISTS (RDOM AB)) $?

⊢ total AB ⇒ ((AB |==> $<=>) |==> $<=>) $? (RES_EXISTS (RRANGE AB))

⊢ bitotal AB ⇒ ((AB |==> $<=>) |==> $<=>) $? $?

⊢ surj AB ⇒ ((AB |==> flip $==>) |==> flip $==>) $? $?

⊢ surj AB ⇒ ((AB |==> $<=>) |==> flip $==>) $? $?

⊢ total AB ⇒ ((AB |==> $<=>) |==> $==>) $? $?

⊢ total AB ⇒ ((AB |==> $==>) |==> $==>) $? $?

⊢ ((CD |==> AB |==> CD) |==> CD |==> LIST_REL AB |==> CD) FOLDL FOLDL

⊢ ((AB |==> CD |==> CD) |==> CD |==> LIST_REL AB |==> CD) FOLDR FOLDR

⊢ ((AB ### CD) |==> AB) FST FST

⊢ ((AB |==> AB) |==> $= |==> AB |==> AB) FUNPOW FUNPOW

⊢ (AB |==> CD) f g ∧ AB a b ⇒ CD (f a) (g b)

⊢ (AB1 |==> CD) f g ∧ AB2 a b ⇒ AB1 = AB2 ⇒ CD (f a) (g b)

⊢ (AB |==> $<=>) P Q ⇒ (AB |==> $==>) P Q ∧ (AB |==> flip $==>) P Q

⊢ ∀R1 R2 f g. (R1 |==> R2) f g ⇔ ∀a b. R1 a b ⇒ R2 (f a) (g b)

⊢ (AB |==> $<=>) P Q ⇒ (AB |==> flip $==>) P Q

⊢ (AB |==> $<=>) P Q ⇒ (AB |==> $==>) P Q

⊢ (LIST_REL AB |==> $=) LENGTH LENGTH

⊢ ((AB |==> CD) |==> AB |==> CD) LET LET

⊢ left_unique AB ⇒ left_unique (LIST_REL AB)

⊢ right_unique AB ⇒ right_unique (LIST_REL AB)

⊢ surj AB ⇒ surj (LIST_REL AB)

⊢ total AB ⇒ total (LIST_REL AB)

⊢ ((AB |==> CD) |==> LIST_REL AB |==> LIST_REL CD) MAP MAP

⊢ LIST_REL AB [] []

⊢ OPTREL AB NONE NONE

⊢ (OPTREL AB |==> (AB |==> OPTREL CD) |==> OPTREL CD) OPTION_BIND
    OPTION_BIND

⊢ ((AB |==> CD) |==> OPTREL AB |==> OPTREL CD) OPTION_MAP OPTION_MAP

⊢ left_unique AB ⇒ left_unique (OPTREL AB)

⊢ right_unique AB ⇒ right_unique (OPTREL AB)

⊢ surj AB ⇒ surj (OPTREL AB)

⊢ total AB ⇒ total (OPTREL AB)

⊢ (AB |==> $= |==> PAIRU AB) $, K

⊢ PAIRU AB (a,()) b = AB a b

⊢ ∀P. (∀AB a b. P AB (a,()) b) ⇒ ∀v v1 v2 v3. P v (v1,v2) v3

⊢ ∀R1 R2. R1 ### R2 = (λ(s,t) (u,v). R1 s u ∧ R2 t v)

⊢ RDOM $= = K T

⊢ RRANGE $= = K T

⊢ ((AB ### CD) |==> CD) SND SND

⊢ (AB |==> OPTREL AB) SOME SOME

⊢ (LIST_REL AB |==> LIST_REL AB) TL TL

⊢ ($= |==> AB |==> UPAIR AB) $, (K I)

⊢ UPAIR AB ((),a) b = AB a b

⊢ ∀P. (∀AB a b. P AB ((),a) b) ⇒ ∀v v1 v2 v3. P v (v1,v2) v3

⊢ () = ()

⊢ bi_unique $=

⊢ left_unique r ∧ right_unique r ⇒ bi_unique r

⊢ bitotal $=

⊢ total r ∧ surj r ⇒ bitotal r

⊢ (flip $==> |==> flip $==> |==> flip $==>) $\/ $\/

⊢ ($==> |==> flip $==> |==> flip $==>) $==> $==>

⊢ equalityp $=

⊢ ($<=> |==> $<=> |==> $<=>) $==> $==>

⊢ equalityp AB ∧ equalityp CD ⇒ equalityp (AB |==> CD)

⊢ equalityp AB ⇒ equalityp (LIST_REL AB)

⊢ equalityp AB ⇒ equalityp (OPTREL AB)

⊢ equalityp AB ∧ equalityp CD ⇒ equalityp (AB ### CD)

⊢ equalityp A ⇒ A x x

⊢ ($==> |==> $==> |==> $==>) $/\ $/\

⊢ ($==> |==> $==> |==> $==>) $\/ $\/

⊢ left_unique $=

⊢ (LIST_REL AB |==> CD |==> (AB |==> LIST_REL AB |==> CD) |==> CD)
    list_CASE list_CASE

⊢ (OPTREL AB |==> CD |==> (AB |==> CD) |==> CD) option_CASE option_CASE

⊢ ((AB ### CD) |==> (AB |==> CD |==> EF) |==> EF) pair_CASE pair_CASE

⊢ right_unique $=

⊢ surj $=

⊢ surj ($= |==> $=)

⊢ surj AB ∧ right_unique AB ⇒ surj (AB |==> $<=>)

⊢ total $=

⊢ total AB ∧ left_unique AB ⇒ total (AB |==> $<=>)