---

Step * of Lemma comb_for_l_all_wf

λT,L,P,z. (∀x∈L.P[x]) ∈ T:Type ⟶ L:(T List) ⟶ P:(T ⟶ ℙ) ⟶ (↓True) ⟶ ℙ
BY
{ (ProveOpCombinatorTyping Auto{1,3}-1) `l_all_wf` }

---

Latex:

---

Latex:
\mlambda{}T,L,P,z.  (\mforall{}x\mmember{}L.P[x])  \mmember{}  T:Type  {}\mrightarrow{}  L:(T  List)  {}\mrightarrow{}  P:(T  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \mBbbP{}


By

---

Latex:
(ProveOpCombinatorTyping  Auto\{1,3\}-1)  `l\_all\_wf`

---

Home Index