---

Step * of Lemma comb_for_lookup_wf

λa,B,z,k,xs,z1. (xs[k]) ∈ a:PosetSig ⟶ B:Type ⟶ z:B ⟶ k:|a| ⟶ xs:((|a| × B) List) ⟶ (↓True) ⟶ B
BY
{ ProveOpCombTyping `lookup_wf` }

---

Latex:

---

Latex:
\mlambda{}a,B,z,k,xs,z1.  (xs[k])  \mmember{}  a:PosetSig  {}\mrightarrow{}  B:Type  {}\mrightarrow{}  z:B  {}\mrightarrow{}  k:|a|  {}\mrightarrow{}  xs:((|a|  \mtimes{}  B)  List)  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \000CB


By

---

Latex:
ProveOpCombTyping  `lookup\_wf`

---

Home Index