---

Step * 1 1 1 1 of Lemma cnv-taba_wf


1. A : Type
2. B : Type
⊢ ∀ys:B List. ((0 ≤ ||ys||) ⇒ (<[], ys> ∈ {p:(A × B) List × (B List)| (0 + ||snd(p)||) = ||ys|| ∈ ℤ} ))
BY
{ (Auto THEN MemTypeCD THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
\mvdash{}  \mforall{}ys:B  List.  ((0  \mleq{}  ||ys||)  {}\mRightarrow{}  (<[],  ys>  \mmember{}  \{p:(A  \mtimes{}  B)  List  \mtimes{}  (B  List)|  (0  +  ||snd(p)||)  =  ||ys||\}  ))


By

---

Latex:
(Auto  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto)

---

Home Index