---

Step * of Lemma cnv-taba-property

∀[A,B:Type].
  ∀xs:A List. ∀ys:B List.  ((||xs|| ≤ ||ys||) ⇒ (cnv-taba(xs;ys) = zip(xs;rev(firstn(||xs||;ys))) ∈ ((A × B) List)))
BY
{ TACTIC:RepeatFor 2 ((D 0 THENA Auto)) }

1
1. A : Type
2. B : Type
⊢ ∀xs:A List. ∀ys:B List.  ((||xs|| ≤ ||ys||) ⇒ (cnv-taba(xs;ys) = zip(xs;rev(firstn(||xs||;ys))) ∈ ((A × B) List)))

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}xs:A  List.  \mforall{}ys:B  List.    ((||xs||  \mleq{}  ||ys||)  {}\mRightarrow{}  (cnv-taba(xs;ys)  =  zip(xs;rev(firstn(||xs||;ys)))))


By

---

Latex:
TACTIC:RepeatFor  2  ((D  0  THENA  Auto))

---

Home Index