---

Step * 1 2 of Lemma not_base_decidble_eq_diag2


1. d : t1,t2:Base.  Dec(t1 = t2)@i
2. t1 : Base@i
3. t2 : Base@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:Base.    Dec(t1  =  t2)@i
2.  t1  :  Base@i
3.  t2  :  Base@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