---

Step * 1 2 1 1 1 of Lemma surject_implies_decidble_eq2


1. T : Type@i'
2. f :   T@i
3. h : b:T. a:. ((f a) = b)@i
4. t1 : T@i
5. t2 : T@i
6. g : T  
7. b:T. ((f (g b)) = b)
8. (g t1) = (g t2)
 t1 = t2
BY
{ ((InstHyp [t1] (-2) THEN Auto THEN D (-1)) THEN InstHyp [t2] (-3) THEN Auto THEN skip{D (-1)}) }



1.  T  :  Type@i'
2.  f  :  \mBbbN{}  {}\mrightarrow{}  T@i
3.  h  :  \mforall{}b:T.  \mexists{}a:\mBbbN{}.  ((f  a)  =  b)@i
4.  t1  :  T@i
5.  t2  :  T@i
6.  g  :  T  {}\mrightarrow{}  \mBbbN{}
7.  \mforall{}b:T.  ((f  (g  b))  =  b)
8.  (g  t1)  =  (g  t2)
\mvdash{}  t1  =  t2


By

((InstHyp  [\mkleeneopen{}t1\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto  THEN  D  (-1))  THEN  InstHyp  [\mkleeneopen{}t2\mkleeneclose{}]  (-3)\mcdot{}  THEN  Auto  THEN  skip\{D  (-1)\})
\mcdot{}



Home Index