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