---

Step * of Lemma lookup_wf

∀a:PosetSig. ∀B:Type. ∀z:B. ∀k:|a|. ∀xs:(|a| × B) List.  (xs[k] ∈ B)
BY
{ ((RepD) THENA Auto) THEN ListInd (-1)  
 }

1
1. a : PosetSig
2. B : Type
3. z : B
4. k : |a|
⊢ [][k] ∈ B

2
1. a : PosetSig
2. B : Type
3. z : B
4. k : |a|
5. u : |a| × B
6. v : (|a| × B) List
7. v[k] ∈ B
⊢ [u / v][k] ∈ B

---

Latex:

---

Latex:
\mforall{}a:PosetSig.  \mforall{}B:Type.  \mforall{}z:B.  \mforall{}k:|a|.  \mforall{}xs:(|a|  \mtimes{}  B)  List.    (xs[k]  \mmember{}  B)


By

---

Latex:
((RepD)  THENA  Auto)  THEN  ListInd  (-1)   

---

Home Index