---

Step * 1 of Lemma not_base_decidble_eq_diag2

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

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

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


.....assertion..... 
1.  \mforall{}t1,t2:Base.    Dec(t1  =  t2)@i
\mvdash{}  \mexists{}eqd:Base  {}\mrightarrow{}  Base  {}\mrightarrow{}  \mBbbB{}.  \mforall{}t1,t2:Base.    (\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)



Home Index