---

Step * of Lemma not_base_decidable_eq_weaker

((t:Base. (((t))  (t)))  (t:Base. (((t ~ bottom()))  (t))))  ((t1,t2:Base.  Dec(t1 = t2)))
BY
{ (Auto THEN D (0) THEN Auto) }

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


((\mforall{}t:Base.  ((\mneg{}\mneg{}(t)\mdownarrow{})  {}\mRightarrow{}  (t)\mdownarrow{}))  \mvee{}  (\mforall{}t:Base.  ((\mneg{}(t  \msim{}  bottom()))  {}\mRightarrow{}  (t)\mdownarrow{})))
{}\mRightarrow{}  (\mneg{}(\mforall{}t1,t2:Base.    Dec(t1  =  t2)))


By

(Auto  THEN  D  (0)  THEN  Auto)



Home Index