---

Step * 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. b : T@i
 (f (fst((h b)))) = b
BY
{ (GenConclAtAddr [2;2;1] THEN DVar `v' THEN MaAuto) }



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.  b  :  T@i
\mvdash{}  (f  (fst((h  b))))  =  b


By

(GenConclAtAddr  [2;2;1]  THEN  DVar  `v'  THEN  MaAuto)



Home Index