---

Step * of Lemma comb_for_cons_wf_listp

λA,l,x,z. [x / l] ∈ A:Type ⟶ l:(A List) ⟶ x:A ⟶ (↓True) ⟶ A List+
BY
{ (ProveOpCombinatorTyping Auto) `cons_wf_listp` }

---

Latex:

---

Latex:
\mlambda{}A,l,x,z.  [x  /  l]  \mmember{}  A:Type  {}\mrightarrow{}  l:(A  List)  {}\mrightarrow{}  x:A  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  A  List\msupplus{}


By

---

Latex:
(ProveOpCombinatorTyping  Auto)  `cons\_wf\_listp`

---

Home Index