---

Step * of Lemma lift-test2

∀[r,g,a:Top].  (let a,b = let a,b = r in <g, a> in a + b ~ let a,b = r in let g,u = <g, a> in g + u)
BY
{ (SymbComp 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[r,g,a:Top].    (let  a,b  =  let  a,b  =  r  in  <g,  a>  in  a  +  b  \msim{}  let  a,b  =  r  in  let  g,u  =  <g,  a>  in  g  +  u)


By

---

Latex:
(SymbComp  0  THEN  Auto)

---

Home Index