---

Step * of Lemma decidable__inject-finite-type

∀[T:Type]
  (finite-type(T)
  ⇒ (∀x,y:T.  Dec(x = y ∈ T))
  ⇒ (∀[A:Type]. ((∀x,y:A.  Dec(x = y ∈ A)) ⇒ (∀f:T ⟶ A. Dec(Inj(T;A;f))))))
BY
{ (Auto
   THEN (FLemma `finite-type-iff-list` [2] THENA Auto)
   THEN ExRepD
   THEN (Assert Inj(T;A;f) ⇐⇒ (∀x∈L.(∀y∈L.((f x) = (f y) ∈ A) ⇒ (x = y ∈ T))) BY
               (RepUR ``inject`` 0 THEN RWW "l_all_iff" 0 THEN Auto THEN Auto'))
   THEN RWO "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    (finite-type(T)
    {}\mRightarrow{}  (\mforall{}x,y:T.    Dec(x  =  y))
    {}\mRightarrow{}  (\mforall{}[A:Type].  ((\mforall{}x,y:A.    Dec(x  =  y))  {}\mRightarrow{}  (\mforall{}f:T  {}\mrightarrow{}  A.  Dec(Inj(T;A;f))))))


By

---

Latex:
(Auto
  THEN  (FLemma  `finite-type-iff-list`  [2]  THENA  Auto)
  THEN  ExRepD
  THEN  (Assert  Inj(T;A;f)  \mLeftarrow{}{}\mRightarrow{}  (\mforall{}x\mmember{}L.(\mforall{}y\mmember{}L.((f  x)  =  (f  y))  {}\mRightarrow{}  (x  =  y)))  BY
                          (RepUR  ``inject``  0  THEN  RWW  "l\_all\_iff"  0  THEN  Auto  THEN  Auto'))
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index