---

Step * of Lemma normalization-spread2

∀[p,F:Top].  (let a,b = p in F[a;b;p] ~ let a,b = p in F[a;b;<a, b>])
BY
{ SqReasoning }

---

Latex:

---

Latex:
\mforall{}[p,F:Top].    (let  a,b  =  p  in  F[a;b;p]  \msim{}  let  a,b  =  p  in  F[a;b;<a,  b>])


By

---

Latex:
SqReasoning

---

Home Index