---

Step * 1 1 of Lemma sym_grp_is_swaps


1. p : Sym(0)
⊢ p = (Π map(λab.let a,b = ab in txpose_perm(a;b);[])) ∈ Sym(0)
BY
{ AbReduce 0 }

1
1. p : Sym(0)
⊢ p = id_perm() ∈ Sym(0)

---

Latex:

---

Latex:

1.  p  :  Sym(0)
\mvdash{}  p  =  (\mPi{}  map(\mlambda{}ab.let  a,b  =  ab  in  txpose\_perm(a;b);[]))


By

---

Latex:
AbReduce  0

---

Home Index