---

Step * 1 1 2 of Lemma enumerable_implies_decidble_eq


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
7. a1,a2:.  (((a1 = a2))  (((f a1) = (f a2))))
 Dec(t1 = t2)
BY
{ ((InstHyp [t1] 4 THEN Auto THEN D (-1)) THEN InstHyp [t2] 4 THEN Auto THEN D (-1) THEN Unfold `decidable` 0) }

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
7. a1,a2:.  (((a1 = a2))  (((f a1) = (f a2))))
8. a : 
9. (f a) = t1
10. a1 : 
11. (f a1) = t2
 (t1 = t2)  ((t1 = t2))



1.  T  :  Type@i'
2.  f  :  \mBbbN{}  {}\mrightarrow{}  T@i
3.  \mforall{}a1,a2:\mBbbN{}.    (((f  a1)  =  (f  a2))  {}\mRightarrow{}  (a1  =  a2))@i
4.  \mforall{}b:T.  \mexists{}a:\mBbbN{}.  ((f  a)  =  b)@i
5.  t1  :  T@i
6.  t2  :  T@i
7.  \mforall{}a1,a2:\mBbbN{}.    ((\mneg{}(a1  =  a2))  {}\mRightarrow{}  (\mneg{}((f  a1)  =  (f  a2))))
\mvdash{}  Dec(t1  =  t2)


By

((InstHyp  [\mkleeneopen{}t1\mkleeneclose{}]  4\mcdot{}  THEN  Auto  THEN  D  (-1))
  THEN  InstHyp  [\mkleeneopen{}t2\mkleeneclose{}]  4\mcdot{}
  THEN  Auto
  THEN  D  (-1)
  THEN  Unfold  `decidable`  0)\mcdot{}



Home Index