---

Step * of Lemma perm_ident

∀[T:Type]. ∀[p:Perm(T)].  ((p O id_perm() = p ∈ Perm(T)) ∧ (id_perm() O p = p ∈ Perm(T)))
BY
{ (GenUnivCD THENA Auto) }

1
1. T : Type
2. p : Perm(T)
⊢ p O id_perm() = p ∈ Perm(T)

2
1. T : Type
2. p : Perm(T)
⊢ id_perm() O p = p ∈ Perm(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[p:Perm(T)].    ((p  O  id\_perm()  =  p)  \mwedge{}  (id\_perm()  O  p  =  p))


By

---

Latex:
(GenUnivCD  THENA  Auto)

---

Home Index