---

Step * of Lemma not_base_decidble_eq_diag2

(t1,t2:Base.  Dec(t1 = t2))
BY
{ ((D 0 THEN Auto) THEN Assert eqd:Base  Base  . t1,t2:Base.  ((eqd t1 t2)  t1 = t2)) }

1
.....assertion..... 
1. t1,t2:Base.  Dec(t1 = t2)@i
 eqd:Base  Base  . t1,t2:Base.  ((eqd t1 t2)  t1 = t2)

2
1. t1,t2:Base.  Dec(t1 = t2)@i
2. eqd:Base  Base  . t1,t2:Base.  ((eqd t1 t2)  t1 = t2)
 False


\mneg{}(\mforall{}t1,t2:Base.    Dec(t1  =  t2))


By

((D  0  THEN  Auto)  THEN  Assert  \mkleeneopen{}\mexists{}eqd:Base  {}\mrightarrow{}  Base  {}\mrightarrow{}  \mBbbB{}.  \mforall{}t1,t2:Base.    (\muparrow{}(eqd  t1  t2)  \mLeftarrow{}{}\mRightarrow{}  t1  =  t2)\mkleeneclose{}\mcdot{})



Home Index