---

Step * of Lemma comb_for_l_succ_wf

λT,l,x,P,z. y = succ(x) in l⇒ P[y] ∈ T:Type ⟶ l:(T List) ⟶ x:T ⟶ P:(T ⟶ ℙ) ⟶ (↓True) ⟶ ℙ
BY
{ (ProveOpCombinatorTyping Auto) `l_succ_wf` }

---

Latex:

---

Latex:
\mlambda{}T,l,x,P,z.  y  =  succ(x)  in  l{}\mRightarrow{}  P[y]  \mmember{}  T:Type  {}\mrightarrow{}  l:(T  List)  {}\mrightarrow{}  x:T  {}\mrightarrow{}  P:(T  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \mBbbP{}


By

---

Latex:
(ProveOpCombinatorTyping  Auto)  `l\_succ\_wf`

---

Home Index