---

Step * of Lemma map-rev-append-top

∀[f,a,b:Top].  (map(f;rev(a) + b) ~ rev(map(f;a)) + map(f;b))
BY
{ ListAccumListIndSq `a' }

1
.....antecedent..... 
1. b : Base
2. a : Base
3. f : Base
⊢ ∀z:Base. strict1(λx.rev(x) + map(f;z))

---

Latex:

---

Latex:
\mforall{}[f,a,b:Top].    (map(f;rev(a)  +  b)  \msim{}  rev(map(f;a))  +  map(f;b))


By

---

Latex:
ListAccumListIndSq  `a'

---

Home Index