---

Step * 1 2 of Lemma is-list-if-has-value-decomp

.....wf..... 
1. t : ListLike
2. (t)↓
3. a1 : 0 = 0 ∈ ℤ
4. t = ((λp.(snd(p))) <inl Ax, Ax>) ∈ (Unit ⋃ (Top × ListLike))
⊢ ispair((λp.(snd(p))) <inl Ax, Ax>) ∈ 𝔹
BY
{ (Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  t  :  ListLike
2.  (t)\mdownarrow{}
3.  a1  :  0  =  0
4.  t  =  ((\mlambda{}p.(snd(p)))  <inl  Ax,  Ax>)
\mvdash{}  ispair((\mlambda{}p.(snd(p)))  <inl  Ax,  Ax>)  \mmember{}  \mBbbB{}


By

---

Latex:
(Reduce  0  THEN  Auto)

---

Home Index