---

Step * of Lemma comb_for_interleaving_wf

λT,L1,L2,L,z. interleaving(T;L1;L2;L) ∈ T:Type ⟶ L1:(T List) ⟶ L2:(T List) ⟶ L:(T List) ⟶ (↓True) ⟶ ℙ
BY
{ (ProveOpCombinatorTyping Auto) `interleaving_wf` }

---

Latex:

---

Latex:
\mlambda{}T,L1,L2,L,z.  interleaving(T;L1;L2;L)  \mmember{}  T:Type  {}\mrightarrow{}  L1:(T  List)  {}\mrightarrow{}  L2:(T  List)  {}\mrightarrow{}  L:(T  List)  {}\mrightarrow{}  (\mdownarrow{}True\000C)  {}\mrightarrow{}  \mBbbP{}


By

---

Latex:
(ProveOpCombinatorTyping  Auto)  `interleaving\_wf`

---

Home Index