- INL_11
-
|- (INL x = INL y) ⇔ (x = y)
- INR_11
-
|- (INR x = INR y) ⇔ (x = y)
- INR_INL_11
-
|- (∀y x. (INL x = INL y) ⇔ (x = y)) ∧ ∀y x. (INR x = INR y) ⇔ (x = y)
- INR_neq_INL
-
|- ∀v1 v2. INR v2 ≠ INL v1
- sum_axiom
-
|- ∀f g. ∃!h. (h o INL = f) ∧ (h o INR = g)
- sum_INDUCT
-
|- ∀P. (∀x. P (INL x)) ∧ (∀y. P (INR y)) ⇒ ∀s. P s
- FORALL_SUM
-
|- (∀s. P s) ⇔ (∀x. P (INL x)) ∧ ∀y. P (INR y)
- EXISTS_SUM
-
|- ∀P. (∃s. P s) ⇔ (∃x. P (INL x)) ∨ ∃y. P (INR y)
- sum_Axiom
-
|- ∀f g. ∃h. (∀x. h (INL x) = f x) ∧ ∀y. h (INR y) = g y
- sum_CASES
-
|- ∀ss. (∃x. ss = INL x) ∨ ∃y. ss = INR y
- sum_distinct
-
|- ∀x y. INL x ≠ INR y
- sum_distinct1
-
|- ∀x y. INR y ≠ INL x
- ISL_OR_ISR
-
|- ∀x. ISL x ∨ ISR x
- INL
-
|- ∀x. ISL x ⇒ (INL (OUTL x) = x)
- INR
-
|- ∀x. ISR x ⇒ (INR (OUTR x) = x)
- sum_case_cong
-
|- ∀M M' f f1.
(M = M') ∧ (∀x. (M' = INL x) ⇒ (f x = f' x)) ∧
(∀y. (M' = INR y) ⇒ (f1 y = f1' y)) ⇒
(sum_CASE M f f1 = sum_CASE M' f' f1')
- SUM_MAP
-
|- ∀f g z. (f ++ g) z = if ISL z then INL (f (OUTL z)) else INR (g (OUTR z))
- SUM_MAP_CASE
-
|- ∀f g z. (f ++ g) z = sum_CASE z (INL o f) (INR o g)
- SUM_MAP_I
-
|- I ++ I = I
- cond_sum_expand
-
|- (∀x y z. ((if P then INR x else INL y) = INR z) ⇔ P ∧ (z = x)) ∧
(∀x y z. ((if P then INR x else INL y) = INL z) ⇔ ¬P ∧ (z = y)) ∧
(∀x y z. ((if P then INL x else INR y) = INL z) ⇔ P ∧ (z = x)) ∧
∀x y z. ((if P then INL x else INR y) = INR z) ⇔ ¬P ∧ (z = y)
- NOT_ISL_ISR
-
|- ∀x. ¬ISL x ⇔ ISR x
- NOT_ISR_ISL
-
|- ∀x. ¬ISR x ⇔ ISL x
- datatype_sum
-
|- DATATYPE (sum INL INR)