---

Step * 1 of Lemma not_funcNbarB_decidable_eq_fullExt

.....assertion..... 
1. t1,t2:  bar().  Dec(t1 = t2)@i
 eqd:  bar()    bar()  . t1,t2:  bar().  ((eqd t1 t2)  t1 = t2)
BY
{ (RenameVar `d' (-1) THEN InstConcl [t1,t2. isl(d t1 t2)] THEN MaAuto) }

1
1. d : t1,t2:  bar().  Dec(t1 = t2)@i
2. t1 :   bar()@i
3. t2 :   bar()@i
4. isl(d t1 t2)@i
 t1 = t2

2
1. d : t1,t2:  bar().  Dec(t1 = t2)@i
2. t1 :   bar()@i
3. t2 :   bar()@i
4. t1 = t2@i
 ((t1,t2. isl(d t1 t2)) t1 t2)


.....assertion..... 
1.  \mforall{}t1,t2:\mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{}).    Dec(t1  =  t2)@i
\mvdash{}  \mexists{}eqd:\mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{})  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{})  {}\mrightarrow{}  \mBbbB{}.  \mforall{}t1,t2:\mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{}).    (\muparrow{}(eqd  t1  t2)  \mLeftarrow{}{}\mRightarrow{}  t1  =  t2)


By

(RenameVar  `d'  (-1)  THEN  InstConcl  [\mkleeneopen{}\mlambda{}t1,t2.  isl(d  t1  t2)\mkleeneclose{}]\mcdot{}  THEN  MaAuto)\mcdot{}



Home Index