---

Step * 2 1 1 of Lemma prod-Leibniz-type


1. A : Type
2. B : Type
3. s1 : A ⟶ A ⟶ ℙ
4. ∀x,y:A.  ((s1 x y) ⇒ (∀z:A. ((s1 x z) ∨ (s1 y z))))
5. ∀x,y:A.  (x = y ∈ A ⇐⇒ ¬(s1 x y))
6. sep : B ⟶ B ⟶ ℙ
7. ∀x,y:B.  ((sep x y) ⇒ (∀z:B. ((sep x z) ∨ (sep y z))))
8. ∀x,y:B.  (x = y ∈ B ⇐⇒ ¬(sep x y))
9. x1 : A
10. x2 : B
11. y1 : A
12. y2 : B
13. x1 = y1 ∈ A
14. x2 = y2 ∈ B
15. (s1 x1 y1) ∨ (sep x2 y2)
⊢ False
BY
{ (D -1 THEN MoveToConcl (-1) THEN Fold `not` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  s1  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}x,y:A.    ((s1  x  y)  {}\mRightarrow{}  (\mforall{}z:A.  ((s1  x  z)  \mvee{}  (s1  y  z))))
5.  \mforall{}x,y:A.    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(s1  x  y))
6.  sep  :  B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}
7.  \mforall{}x,y:B.    ((sep  x  y)  {}\mRightarrow{}  (\mforall{}z:B.  ((sep  x  z)  \mvee{}  (sep  y  z))))
8.  \mforall{}x,y:B.    (x  =  y  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(sep  x  y))
9.  x1  :  A
10.  x2  :  B
11.  y1  :  A
12.  y2  :  B
13.  x1  =  y1
14.  x2  =  y2
15.  (s1  x1  y1)  \mvee{}  (sep  x2  y2)
\mvdash{}  False


By

---

Latex:
(D  -1  THEN  MoveToConcl  (-1)  THEN  Fold  `not`  0  THEN  Auto)

---

Home Index