---

Step * of Lemma prod-Leibniz-type

∀A,B:Type.  (Leibniz-type{i:l}(A) ⇒ Leibniz-type{i:l}(B) ⇒ Leibniz-type{i:l}(A × B))
BY
{ (Auto
   THEN All (Unfold `Leibniz-type`)
   THEN ExRepD
   THEN (D 0 With ⌜λp,q. ((s1 (fst(p)) (fst(q))) ∨ (sep (snd(p)) (snd(q))))⌝  THENW Auto)
   THEN Reduce 0
   THEN D 0
   THEN (UnivCD THENA Auto)
   THEN DVar `x'
   THEN DVar `y'
   THEN Try (DVar `z')
   THEN All Reduce) }

1
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. (s1 x1 y1) ∨ (sep x2 y2)
14. z1 : A
15. z2 : B
⊢ ((s1 x1 z1) ∨ (sep x2 z2)) ∨ (s1 y1 z1) ∨ (sep y2 z2)

2
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
⊢ <x1, x2> = <y1, y2> ∈ (A × B) ⇐⇒ ¬((s1 x1 y1) ∨ (sep x2 y2))

---

Latex:

---

Latex:
\mforall{}A,B:Type.    (Leibniz-type\{i:l\}(A)  {}\mRightarrow{}  Leibniz-type\{i:l\}(B)  {}\mRightarrow{}  Leibniz-type\{i:l\}(A  \mtimes{}  B))


By

---

Latex:
(Auto
  THEN  All  (Unfold  `Leibniz-type`)
  THEN  ExRepD
  THEN  (D  0  With  \mkleeneopen{}\mlambda{}p,q.  ((s1  (fst(p))  (fst(q)))  \mvee{}  (sep  (snd(p))  (snd(q))))\mkleeneclose{}    THENW  Auto)
  THEN  Reduce  0
  THEN  D  0
  THEN  (UnivCD  THENA  Auto)
  THEN  DVar  `x'
  THEN  DVar  `y'
  THEN  Try  (DVar  `z')
  THEN  All  Reduce)

---

Home Index