---

Step * of Lemma lift-simple-decide-decide1

∀[X,F,G,M,N:Top].
  (case case X of inl(x) => inr F[x]  | inr(x) => inl G[x] of inl(a) => M[a] | inr(b) => N[b] ~ case X
   of inl(x) =>
   N[F[x]]
   | inr(x) =>
   M[G[x]])
BY
{ ((UnivCD THENA Auto) THEN RW LiftAllC 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X,F,G,M,N:Top].
    (case  case  X  of  inl(x)  =>  inr  F[x]    |  inr(x)  =>  inl  G[x]  of  inl(a)  =>  M[a]  |  inr(b)  =>  N[b] 
    \msim{}  case  X  of  inl(x)  =>  N[F[x]]  |  inr(x)  =>  M[G[x]])


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RW  LiftAllC  0  THEN  Auto)

---

Home Index