---

Step * 1 1 of Lemma not_funcNbarB_decidable_eq_fullExt


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
BY
{ (GenHypAtAddr (-1) [1;1] THEN Unfold `decidable` 4 THEN DVar `v' THEN Auto THEN  MaAuto) }



1.  d  :  \mforall{}t1,t2:\mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{}).    Dec(t1  =  t2)@i
2.  t1  :  \mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{})@i
3.  t2  :  \mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{})@i
4.  \muparrow{}isl(d  t1  t2)@i
\mvdash{}  t1  =  t2


By

(GenHypAtAddr  (-1)  [1;1]  THEN  Unfold  `decidable`  4  THEN  DVar  `v'  THEN  Auto  THEN    MaAuto)



Home Index