---

Step * of Lemma rev-zip_wf

∀[A,B:Type]. ∀[L1:A List]. ∀[L2:B List].  (rev-zip(L1;L2) ∈ (A × B) List)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[L1:A  List].  \mforall{}[L2:B  List].    (rev-zip(L1;L2)  \mmember{}  (A  \mtimes{}  B)  List)


By

---

Latex:
ProveWfLemma

---

Home Index