---

Step * of Lemma surject_implies_decidble_eq2

T:Type. ((f:  T. Surj(;T;f))  (t1,t2:T.  Dec(t1 = t2)))
BY
{ ((Auto THEN Unfold `surject` 2) THEN D 2 THEN Unfold `decidable` 0) }

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


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


By

((Auto  THEN  Unfold  `surject`  2)  THEN  D  2  THEN  Unfold  `decidable`  0)



Home Index