---

Step * of Lemma lifting-isaxiom-decide

∀[a,b,c,F,G:Top].
  (if case a of inl(x) => F[x] | inr(x) => G[x] = Ax then b otherwise c ~ case a
   of inl(x) =>
   if F[x] = Ax then b otherwise c
   | inr(x) =>
   if G[x] = Ax then b otherwise c)
BY
{ ProveLiftingLemma }

---

Latex:

---

Latex:
\mforall{}[a,b,c,F,G:Top].
    (if  case  a  of  inl(x)  =>  F[x]  |  inr(x)  =>  G[x]  =  Ax  then  b  otherwise  c  \msim{}  case  a
      of  inl(x)  =>
      if  F[x]  =  Ax  then  b  otherwise  c
      |  inr(x)  =>
      if  G[x]  =  Ax  then  b  otherwise  c)


By

---

Latex:
ProveLiftingLemma

---

Home Index