---

Step * 1 2 of Lemma perm_morph_wf


1. S : Type
2. T : Type
3. s2t : S ⟶ T
4. t2s : T ⟶ S
5. (t2s o s2t) = Id{S} ∈ (S ⟶ S)
6. (s2t o t2s) = Id{T} ∈ (T ⟶ T)
7. p : Perm(S)
8. (p.b o p.f) = Id{S} ∈ (S ⟶ S)
9. (p.f o p.b) = Id{S} ∈ (S ⟶ S)
⊢ ((s2t o (p.f o t2s)) o (s2t o (p.b o t2s))) = Id{T} ∈ (T ⟶ T)
BY
{ (RW (CompIdHypNormC [5; 6; 8; 9]) 0 THEN Auto) }

---

Latex:

---

Latex:

1.  S  :  Type
2.  T  :  Type
3.  s2t  :  S  {}\mrightarrow{}  T
4.  t2s  :  T  {}\mrightarrow{}  S
5.  (t2s  o  s2t)  =  Id\{S\}
6.  (s2t  o  t2s)  =  Id\{T\}
7.  p  :  Perm(S)
8.  (p.b  o  p.f)  =  Id\{S\}
9.  (p.f  o  p.b)  =  Id\{S\}
\mvdash{}  ((s2t  o  (p.f  o  t2s))  o  (s2t  o  (p.b  o  t2s)))  =  Id\{T\}


By

---

Latex:
(RW  (CompIdHypNormC  [5;  6;  8;  9])  0  THEN  Auto)

---

Home Index