---

Step * of Lemma comb_for_swap_wf

λT,L,i,j,z. swap(L;i;j) ∈ T:Type ⟶ L:(T List) ⟶ i:ℕ||L|| ⟶ j:ℕ||L|| ⟶ (↓True) ⟶ (T List)
BY
{ (ProveOpCombinatorTyping Auto) `swap_wf` }

---

Latex:

---

Latex:
\mlambda{}T,L,i,j,z.  swap(L;i;j)  \mmember{}  T:Type  {}\mrightarrow{}  L:(T  List)  {}\mrightarrow{}  i:\mBbbN{}||L||  {}\mrightarrow{}  j:\mBbbN{}||L||  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  (T  List)


By

---

Latex:
(ProveOpCombinatorTyping  Auto)  `swap\_wf`

---

Home Index