---

Step * of Lemma enumerable_implies_decidble_eq

T:Type. ((f:  T. Bij(;T;f))  (t1,t2:T.  Dec(t1 = t2)))
BY
{ Auto }

1
.....decidable?..... 
1. T : Type@i'
2. f:  T. Bij(;T;f)@i
3. t1 : T@i
4. t2 : T@i
 Dec(t1 = t2)


\mforall{}T:Type.  ((\mexists{}f:\mBbbN{}  {}\mrightarrow{}  T.  Bij(\mBbbN{};T;f))  {}\mRightarrow{}  (\mforall{}t1,t2:T.    Dec(t1  =  t2)))


By

Auto



Home Index