---

Step * of Lemma decidable__equal_product

∀[A:Type]. ∀[B:A ⟶ Type].
  ((∀a,b:A.  Dec(a = b ∈ A)) ⇒ (∀a:A. ∀u,v:B[a].  Dec(u = v ∈ B[a])) ⇒ (∀x,y:a:A × B[a].  Dec(x = y ∈ (a:A × B[a]))))
BY
{ (Auto THEN DProds THEN (Decide ⌜a = a1 ∈ A⌝⋅ THENA Auto)) }

1
1. [A] : Type
2. [B] : A ⟶ Type
3. ∀a,b:A.  Dec(a = b ∈ A)
4. ∀a:A. ∀u,v:B[a].  Dec(u = v ∈ B[a])
5. a1 : A
6. x1 : B[a1]
7. a : A
8. y1 : B[a]
9. a = a1 ∈ A
⊢ Dec(<a1, x1> = <a, y1> ∈ (a:A × B[a]))

2
1. [A] : Type
2. [B] : A ⟶ Type
3. ∀a,b:A.  Dec(a = b ∈ A)
4. ∀a:A. ∀u,v:B[a].  Dec(u = v ∈ B[a])
5. a1 : A
6. x1 : B[a1]
7. a : A
8. y1 : B[a]
9. ¬(a = a1 ∈ A)
⊢ Dec(<a1, x1> = <a, y1> ∈ (a:A × B[a]))

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
    ((\mforall{}a,b:A.    Dec(a  =  b))  {}\mRightarrow{}  (\mforall{}a:A.  \mforall{}u,v:B[a].    Dec(u  =  v))  {}\mRightarrow{}  (\mforall{}x,y:a:A  \mtimes{}  B[a].    Dec(x  =  y)))


By

---

Latex:
(Auto  THEN  DProds  THEN  (Decide  \mkleeneopen{}a  =  a1\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index