---

Step * 1 of Lemma cnv-taba_wf


1. A : Type
2. B : Type
⊢ ∀xs:A List. ∀ys:B List.  ((||xs|| ≤ ||ys||) ⇒ (cnv-taba(xs;ys) ∈ (A × B) List))
BY
{ xxxUnfold `cnv-taba` 0xxx }

1
1. A : Type
2. B : Type
⊢ ∀xs:A List. ∀ys:B List.
    ((||xs|| ≤ ||ys||)
    ⇒ (fst(rec-case(xs) of
            [] => <[], ys>
            x::xs' =>
             p.let a,ys = p 
               in let h,t = ys 
                  in <[<x, h> / a], t>) ∈ (A × B) List))

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
\mvdash{}  \mforall{}xs:A  List.  \mforall{}ys:B  List.    ((||xs||  \mleq{}  ||ys||)  {}\mRightarrow{}  (cnv-taba(xs;ys)  \mmember{}  (A  \mtimes{}  B)  List))


By

---

Latex:
xxxUnfold  `cnv-taba`  0xxx

---

Home Index