---

Step * of Lemma comb_for_sublist_wf

λT,L1,L2,z. L1 ⊆ L2 ∈ T:Type ⟶ L1:(T List) ⟶ L2:(T List) ⟶ (↓True) ⟶ ℙ
BY
{ (ProveOpCombinatorTyping Auto) `sublist_wf` }

---

Latex:

---

Latex:
\mlambda{}T,L1,L2,z.  L1  \msubseteq{}  L2  \mmember{}  T:Type  {}\mrightarrow{}  L1:(T  List)  {}\mrightarrow{}  L2:(T  List)  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \mBbbP{}


By

---

Latex:
(ProveOpCombinatorTyping  Auto)  `sublist\_wf`

---

Home Index