---

Step * 1 1 of Lemma perm_igrp_wf


1. T : Type
⊢ Assoc(Perm(T);λp,q. p O q)
BY
{ (Unfold `assoc` 0 THEN AbReduce 0) }

1
1. T : Type
⊢ ∀[x,y,z:Perm(T)].  (x O y O z = x O y O z ∈ Perm(T))

---

Latex:

---

Latex:

1.  T  :  Type
\mvdash{}  Assoc(Perm(T);\mlambda{}p,q.  p  O  q)


By

---

Latex:
(Unfold  `assoc`  0  THEN  AbReduce  0)

---

Home Index