---

Step * 1 of Lemma not_base_decidable_eq_weaker


1. (t:Base. (((t))  (t)))  (t:Base. (((t ~ bottom()))  (t)))@i
2. t1,t2:Base.  Dec(t1 = t2)@i
 False
BY
{ Assert (t:Base. ((t)  ((t)))) }

1
.....assertion..... 
1. (t:Base. (((t))  (t)))  (t:Base. (((t ~ bottom()))  (t)))@i
2. t1,t2:Base.  Dec(t1 = t2)@i
 (t:Base. ((t)  ((t))))

2
1. (t:Base. (((t))  (t)))  (t:Base. (((t ~ bottom()))  (t)))@i
2. t1,t2:Base.  Dec(t1 = t2)@i
3. (t:Base. ((t)  ((t))))
 False



1.  (\mforall{}t:Base.  ((\mneg{}\mneg{}(t)\mdownarrow{})  {}\mRightarrow{}  (t)\mdownarrow{}))  \mvee{}  (\mforall{}t:Base.  ((\mneg{}(t  \msim{}  bottom()))  {}\mRightarrow{}  (t)\mdownarrow{}))@i
2.  \mforall{}t1,t2:Base.    Dec(t1  =  t2)@i
\mvdash{}  False


By

Assert  \mkleeneopen{}\mneg{}(\mforall{}t:Base.  ((t)\mdownarrow{}  \mvee{}  (\mneg{}(t)\mdownarrow{})))\mkleeneclose{}\mcdot{}



Home Index