Step * of Lemma decide-decide2

[x:Top Top]. ∀[f1,f2,h:Top].
  (case of inl(z) => case of inl(z) => f1[z] inr(z) => f2[z] inr(z) => h[z] case x
   of inl(z) =>
   f1[z]
   inr(z) =>
   h[z])
BY
((D THENA Auto) THEN -1 THEN Reduce THEN Auto) }


Latex:


Latex:
\mforall{}[x:Top  +  Top].  \mforall{}[f1,f2,h:Top].
    (case  x  of  inl(z)  =>  case  x  of  inl(z)  =>  f1[z]  |  inr(z)  =>  f2[z]  |  inr(z)  =>  h[z]  \msim{}  case  x
      of  inl(z)  =>
      f1[z]
      |  inr(z)  =>
      h[z])


By


Latex:
((D  0  THENA  Auto)  THEN  D  -1  THEN  Reduce  0  THEN  Auto)




Home Index