---

Step * 1 of Lemma length-rev-append


1. bs : Base
2. as : Base
3. z : Base@i
⊢ strict1(λx.(x + ||z||))
BY
{ (ProveStrict THEN Auto) }

---

Latex:

---

Latex:

1.  bs  :  Base
2.  as  :  Base
3.  z  :  Base@i
\mvdash{}  strict1(\mlambda{}x.(x  +  ||z||))


By

---

Latex:
(ProveStrict  THEN  Auto)

---

Home Index