---

Step * of Lemma product-Leibniz-type

∀A:Type. ∀B:A ⟶ Type.  ((∀x,y:A.  Dec(x = y ∈ A)) ⇒ (∀a:A. Leibniz-type{i:l}(B[a])) ⇒ Leibniz-type{i:l}(a:A × B[a]))
BY
{ (Auto THEN All (Unfold `Leibniz-type`) THEN (Skolemize (-1) `s'  THENA Auto)) }

1
1. A : Type
2. B : A ⟶ Type
3. ∀x,y:A.  Dec(x = y ∈ A)
4. ∀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))))
5. s : a:A ⟶ B[a] ⟶ B[a] ⟶ ℙ
6. ∀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))))

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}B:A  {}\mrightarrow{}  Type.
    ((\mforall{}x,y:A.    Dec(x  =  y))  {}\mRightarrow{}  (\mforall{}a:A.  Leibniz-type\{i:l\}(B[a]))  {}\mRightarrow{}  Leibniz-type\{i:l\}(a:A  \mtimes{}  B[a]))


By

---

Latex:
(Auto  THEN  All  (Unfold  `Leibniz-type`)  THEN  (Skolemize  (-1)  `s'    THENA  Auto))

---

Home Index