---

Step * 1 of Lemma function-Leibniz-type


1. A : Type
2. B : A ⟶ Type
3. ∀a:A
     ∃sep:B[a] ⟶ B[a] ⟶ ℙ
      ((∀x,y:B[a].  ((sep x y) ⇒ (∀z:B[a]. ((sep x z) ∨ (sep y z))))) ∧ (∀x,y:B[a].  (x = y ∈ B[a] ⇐⇒ ¬(sep x y))))
4. s : a:A ⟶ B[a] ⟶ B[a] ⟶ ℙ
5. ∀a:A. ((∀x,y:B[a].  ((s a x y) ⇒ (∀z:B[a]. ((s a x z) ∨ (s a y z))))) ∧ (∀x,y:B[a].  (x = y ∈ B[a] ⇐⇒ ¬(s a x y))))
⊢ ∃sep:(a:A ⟶ B[a]) ⟶ (a:A ⟶ B[a]) ⟶ ℙ
   ((∀x,y:a:A ⟶ B[a].  ((sep x y) ⇒ (∀z:a:A ⟶ B[a]. ((sep x z) ∨ (sep y z)))))
   ∧ (∀x,y:a:A ⟶ B[a].  (x = y ∈ (a:A ⟶ B[a]) ⇐⇒ ¬(sep x y))))
BY
{ (D 0 With ⌜λf,g. ∃a:A. (s a (f a) (g a))⌝  THEN (Reduce 0 THENW Auto) THEN D 0 THEN (UnivCD THENA Auto)) }

1
1. A : Type
2. B : A ⟶ Type
3. ∀a:A
     ∃sep:B[a] ⟶ B[a] ⟶ ℙ
      ((∀x,y:B[a].  ((sep x y) ⇒ (∀z:B[a]. ((sep x z) ∨ (sep y z))))) ∧ (∀x,y:B[a].  (x = y ∈ B[a] ⇐⇒ ¬(sep x y))))
4. s : a:A ⟶ B[a] ⟶ B[a] ⟶ ℙ
5. ∀a:A. ((∀x,y:B[a].  ((s a x y) ⇒ (∀z:B[a]. ((s a x z) ∨ (s a y z))))) ∧ (∀x,y:B[a].  (x = y ∈ B[a] ⇐⇒ ¬(s a x y))))
6. x : a:A ⟶ B[a]
7. y : a:A ⟶ B[a]
8. ∃a:A. (s a (x a) (y a))
9. z : a:A ⟶ B[a]
⊢ (∃a:A. (s a (x a) (z a))) ∨ (∃a:A. (s a (y a) (z a)))

2
1. A : Type
2. B : A ⟶ Type
3. ∀a:A
     ∃sep:B[a] ⟶ B[a] ⟶ ℙ
      ((∀x,y:B[a].  ((sep x y) ⇒ (∀z:B[a]. ((sep x z) ∨ (sep y z))))) ∧ (∀x,y:B[a].  (x = y ∈ B[a] ⇐⇒ ¬(sep x y))))
4. s : a:A ⟶ B[a] ⟶ B[a] ⟶ ℙ
5. ∀a:A. ((∀x,y:B[a].  ((s a x y) ⇒ (∀z:B[a]. ((s a x z) ∨ (s a y z))))) ∧ (∀x,y:B[a].  (x = y ∈ B[a] ⇐⇒ ¬(s a x y))))
6. x : a:A ⟶ B[a]
7. y : a:A ⟶ B[a]
⊢ x = y ∈ (a:A ⟶ B[a]) ⇐⇒ ¬(∃a:A. (s a (x a) (y a)))

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  \mforall{}a:A
          \mexists{}sep:B[a]  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  \mBbbP{}
            ((\mforall{}x,y:B[a].    ((sep  x  y)  {}\mRightarrow{}  (\mforall{}z:B[a].  ((sep  x  z)  \mvee{}  (sep  y  z)))))
            \mwedge{}  (\mforall{}x,y:B[a].    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(sep  x  y))))
4.  s  :  a:A  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}a:A
          ((\mforall{}x,y:B[a].    ((s  a  x  y)  {}\mRightarrow{}  (\mforall{}z:B[a].  ((s  a  x  z)  \mvee{}  (s  a  y  z)))))
          \mwedge{}  (\mforall{}x,y:B[a].    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(s  a  x  y))))
\mvdash{}  \mexists{}sep:(a:A  {}\mrightarrow{}  B[a])  {}\mrightarrow{}  (a:A  {}\mrightarrow{}  B[a])  {}\mrightarrow{}  \mBbbP{}
      ((\mforall{}x,y:a:A  {}\mrightarrow{}  B[a].    ((sep  x  y)  {}\mRightarrow{}  (\mforall{}z:a:A  {}\mrightarrow{}  B[a].  ((sep  x  z)  \mvee{}  (sep  y  z)))))
      \mwedge{}  (\mforall{}x,y:a:A  {}\mrightarrow{}  B[a].    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(sep  x  y))))


By

---

Latex:
(D  0  With  \mkleeneopen{}\mlambda{}f,g.  \mexists{}a:A.  (s  a  (f  a)  (g  a))\mkleeneclose{}    THEN  (Reduce  0  THENW  Auto)  THEN  D  0  THEN  (UnivCD  THENA  Au\000Cto))

---

Home Index