---

Step * of Lemma comb_for_ball_wf

λA,as,f,z. ∀bx(:A) ∈ as. f[x] ∈ A:Type ⟶ as:(A List) ⟶ f:(A ⟶ 𝔹) ⟶ (↓True) ⟶ 𝔹
BY
{ (ProveOpCombinatorTyping Auto) `ball_wf` }

---

Latex:

---

Latex:
\mlambda{}A,as,f,z.  \mforall{}\msubb{}x(:A)  \mmember{}  as.  f[x]  \mmember{}  A:Type  {}\mrightarrow{}  as:(A  List)  {}\mrightarrow{}  f:(A  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \mBbbB{}


By

---

Latex:
(ProveOpCombinatorTyping  Auto)  `ball\_wf`

---

Home Index