---

Step * of Lemma fpf-ap-compose

∀[x:Top]. ∀[f:a:Top fp-> Top]. ∀[g,eq:Top].  (g o f(x) ~ g f(x))
BY
{ (Reduce 0 THEN Auto) }

---

Latex:


\mforall{}[x:Top].  \mforall{}[f:a:Top  fp->  Top].  \mforall{}[g,eq:Top].    (g  o  f(x)  \msim{}  g  f(x))


By

(Reduce  0  THEN  Auto)

---

Home Index