---

Step * of Lemma int-prod-single

∀[f:Top]. (Π(f[x] | x < 1) ~ 1 * f[0])
BY
{ xxx((Auto THEN (RWO "int-prod-unroll-hi" 0 THENA Auto)) THEN Reduce 0 THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[f:Top].  (\mPi{}(f[x]  |  x  <  1)  \msim{}  1  *  f[0])


By

---

Latex:
xxx((Auto  THEN  (RWO  "int-prod-unroll-hi"  0  THENA  Auto))  THEN  Reduce  0  THEN  Auto)xxx

---

Home Index