---

Step * 1 2 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. t1 = t2@i
 ((t1,t2. isl(d t1 t2)) t1 t2)
BY
{ (Reduce 0 THEN GenHypAtAddr (0) [1;1] THEN Unfold `decidable` (-2) 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.  t1  =  t2@i
\mvdash{}  \muparrow{}((\mlambda{}t1,t2.  isl(d  t1  t2))  t1  t2)


By

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



Home Index