---

Step * of Lemma accumulate_abort_nil_lemma

∀s,F:Top.  (accumulate_abort(x,y.F[x;y];s;[]) ~ s)
BY
{ ((UnivCD THENA Auto) THEN SqequalBySymbComp200) }

---

Latex:

---

Latex:
\mforall{}s,F:Top.    (accumulate\_abort(x,y.F[x;y];s;[])  \msim{}  s)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  SqequalBySymbComp200)

---

Home Index