---

Step * of Lemma lift-test

∀[t:Top]
  ((let x,y = let a,b = t 
              in <b, a> 
    in x + y ~ let a,b = t 
               in b + a)
  ∧ (let x,y = case t of inl(a) => <1, 2> | inr(b) => <3, 4> 
     in x + y ~ case t of inl(a) => 3 | inr(b) => 7)
  ∧ (let x,y = if t=33  then <1, 2>  else <3, 4> 
     in x + y ~ if t=33  then 3  else 7))
BY
{ (SymbComp 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[t:Top]
    ((let  x,y  =  let  a,b  =  t 
                            in  <b,  a> 
        in  x  +  y  \msim{}  let  a,b  =  t 
                              in  b  +  a)
    \mwedge{}  (let  x,y  =  case  t  of  inl(a)  =>  ə,  2>  |  inr(b)  =>  ɛ,  4> 
          in  x  +  y  \msim{}  case  t  of  inl(a)  =>  3  |  inr(b)  =>  7)
    \mwedge{}  (let  x,y  =  if  t=33    then  ə,  2>    else  ɛ,  4> 
          in  x  +  y  \msim{}  if  t=33    then  3    else  7))


By

---

Latex:
(SymbComp  0  THEN  Auto)

---

Home Index