---

Step * of Lemma test-lifting

∀x:Top. (if isl(x) then 1 + outl(x) else 2 fi  ~ case x of inl(y) => 1 + y | inr(z) => 2)
BY
{ ((D 0 THENA Auto) THEN (SymbComp 0 THEN LiftRed) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x:Top.  (if  isl(x)  then  1  +  outl(x)  else  2  fi    \msim{}  case  x  of  inl(y)  =>  1  +  y  |  inr(z)  =>  2)


By

---

Latex:
((D  0  THENA  Auto)  THEN  (SymbComp  0  THEN  LiftRed)  THEN  Auto)

---

Home Index