---

Step * of Lemma decidable__equal_compact_domain

∀[T,S:Type].  ((∀a,b:S.  Dec(a = b ∈ S)) ⇒ compact-type(T) ⇒ (∀f,g:T ⟶ S.  Dec(f = g ∈ (T ⟶ S))))
BY
{ (Auto THEN (FLemma `deq-exists` [3] THENA Auto) THEN RenameVar `eq' (-1)) }

1
1. [T] : Type
2. [S] : Type
3. ∀a,b:S.  Dec(a = b ∈ S)
4. compact-type(T)
5. f : T ⟶ S
6. g : T ⟶ S
7. eq : EqDecider(S)
⊢ Dec(f = g ∈ (T ⟶ S))

---

Latex:

---

Latex:
\mforall{}[T,S:Type].    ((\mforall{}a,b:S.    Dec(a  =  b))  {}\mRightarrow{}  compact-type(T)  {}\mRightarrow{}  (\mforall{}f,g:T  {}\mrightarrow{}  S.    Dec(f  =  g)))


By

---

Latex:
(Auto  THEN  (FLemma  `deq-exists`  [3]  THENA  Auto)  THEN  RenameVar  `eq'  (-1))

---

Home Index