---

Step * 1 of Lemma enumerable_implies_decidble_eq

.....decidable?..... 
1. T : Type@i'
2. f:  T. Bij(;T;f)@i
3. t1 : T@i
4. t2 : T@i
 Dec(t1 = t2)
BY
{ (D 2 THEN RepUR ``biject surject inject`` (3) THEN D (3)) }

1
1. T : Type@i'
2. f :   T@i
3. a1,a2:.  (((f a1) = (f a2))  (a1 = a2))@i
4. b:T. a:. ((f a) = b)@i
5. t1 : T@i
6. t2 : T@i
 Dec(t1 = t2)


.....decidable?..... 
1.  T  :  Type@i'
2.  \mexists{}f:\mBbbN{}  {}\mrightarrow{}  T.  Bij(\mBbbN{};T;f)@i
3.  t1  :  T@i
4.  t2  :  T@i
\mvdash{}  Dec(t1  =  t2)


By

(D  2  THEN  RepUR  ``biject  surject  inject``  (3)  THEN  D  (3))



Home Index