---

Step * of Lemma decidable__equal_equipollent

∀[T:Type]. ∀k:ℕ. (T ~ ℕk ⇒ (∀a,b:T.  Dec(a = b ∈ T)))
BY
{ (Auto THEN D 3 THEN ((Decide ⌜(f a) = (f b) ∈ ℕk⌝⋅ THENA Auto) THENL [OrLeft; OrRight]) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}k:\mBbbN{}.  (T  \msim{}  \mBbbN{}k  {}\mRightarrow{}  (\mforall{}a,b:T.    Dec(a  =  b)))


By

---

Latex:
(Auto  THEN  D  3  THEN  ((Decide  \mkleeneopen{}(f  a)  =  (f  b)\mkleeneclose{}\mcdot{}  THENA  Auto)  THENL  [OrLeft;  OrRight])  THEN  Auto)

---

Home Index