---

Step * of Lemma cnv-taba_wf

∀[A,B:Type].  ∀xs:A List. ∀ys:B List.  ((||xs|| ≤ ||ys||) ⇒ (cnv-taba(xs;ys) ∈ (A × B) List))
BY
{ xxxRepeatFor 2 ((D 0 THENA Auto))xxx }

1
1. A : Type
2. B : Type
⊢ ∀xs:A List. ∀ys:B List.  ((||xs|| ≤ ||ys||) ⇒ (cnv-taba(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)  \mmember{}  (A  \mtimes{}  B)  List))


By

---

Latex:
xxxRepeatFor  2  ((D  0  THENA  Auto))xxx

---

Home Index