---

Step * 2 1 of Lemma not_base_decidble_eq_diag2

.....assertion..... 
1. t1,t2:Base.  Dec(t1 = t2)@i
2. eqd : Base  Base  
3. t1,t2:Base.  ((eqd t1 t2)  t1 = t2)
 isBot:Base  . t:Base. ((isBot t)  t = bottom())
BY
{ (InstConcl [t.(eqd t bottom())] THEN MaAuto THEN Reduce 0 THEN MaAuto) }


.....assertion..... 
1.  \mforall{}t1,t2:Base.    Dec(t1  =  t2)@i
2.  eqd  :  Base  {}\mrightarrow{}  Base  {}\mrightarrow{}  \mBbbB{}
3.  \mforall{}t1,t2:Base.    (\muparrow{}(eqd  t1  t2)  \mLeftarrow{}{}\mRightarrow{}  t1  =  t2)
\mvdash{}  \mexists{}isBot:Base  {}\mrightarrow{}  \mBbbB{}.  \mforall{}t:Base.  (\muparrow{}(isBot  t)  \mLeftarrow{}{}\mRightarrow{}  t  =  bottom())


By

(InstConcl  [\mkleeneopen{}\mlambda{}t.(eqd  t  bottom())\mkleeneclose{}]\mcdot{}  THEN  MaAuto  THEN  Reduce  0  THEN  MaAuto)\mcdot{}



Home Index