---

Step * 1 of Lemma map-rev-append-top

.....antecedent..... 
1. b : Base
2. a : Base
3. f : Base
⊢ ∀z:Base. strict1(λx.rev(x) + map(f;z))
BY
{ (Auto THEN ProveStrict THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  b  :  Base
2.  a  :  Base
3.  f  :  Base
\mvdash{}  \mforall{}z:Base.  strict1(\mlambda{}x.rev(x)  +  map(f;z))


By

---

Latex:
(Auto  THEN  ProveStrict  THEN  Auto)

---

Home Index