---

Step * 1 of Lemma surject_implies_decidble_eq2


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))
BY
{ ((Assert g:T  . b:T. ((f (g b)) = b) THEN Auto) THEN RenameVar  `h' 3) }

1
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
 g:T  . b:T. ((f (g b)) = b)

2
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  . b:T. ((f (g b)) = b)
 (t1 = t2)  ((t1 = t2))



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


By

((Assert  \mkleeneopen{}\mexists{}g:T  {}\mrightarrow{}  \mBbbN{}.  \mforall{}b:T.  ((f  (g  b))  =  b)\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  RenameVar    `h'  3)



Home Index