---

Step * 1 2 of Lemma perm_igrp_wf


1. T : Type
⊢ Ident(Perm(T);λp,q. p O q;id_perm())
BY
{ ((Unfold `ident` 0 THEN AbReduce 0) THEN MoveToConcl 1) }

1
∀T:Type. ∀[x:Perm(T)]. ((x O id_perm() = x ∈ Perm(T)) ∧ (id_perm() O x = x ∈ Perm(T)))

---

Latex:

---

Latex:

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


By

---

Latex:
((Unfold  `ident`  0  THEN  AbReduce  0)  THEN  MoveToConcl  1)

---

Home Index