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