---

Step * of Lemma comb_for_txpose_perm_wf

λn,i,j,z. txpose_perm(i;j) ∈ n:ℕ ⟶ i:ℕn ⟶ j:ℕn ⟶ (↓True) ⟶ Sym(n)
BY
{ (ProveOpCombinatorTyping Auto) `txpose_perm_wf` }

---

Latex:

---

Latex:
\mlambda{}n,i,j,z.  txpose\_perm(i;j)  \mmember{}  n:\mBbbN{}  {}\mrightarrow{}  i:\mBbbN{}n  {}\mrightarrow{}  j:\mBbbN{}n  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  Sym(n)


By

---

Latex:
(ProveOpCombinatorTyping  Auto)  `txpose\_perm\_wf`

---

Home Index