---

Step * of Lemma comb_for_count_wf

λs,a,bs,z. (a #∈ bs) ∈ s:DSet ⟶ a:|s| ⟶ bs:(|s| List) ⟶ (↓True) ⟶ ℤ
BY
{ Auto }

---

Latex:

---

Latex:
\mlambda{}s,a,bs,z.  (a  \#\mmember{}  bs)  \mmember{}  s:DSet  {}\mrightarrow{}  a:|s|  {}\mrightarrow{}  bs:(|s|  List)  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \mBbbZ{}


By

---

Latex:
Auto

---

Home Index