---

Step * of Lemma perm_b_to_f

∀T:Type. ∀p:Perm(T). ∀x,y:T.  ((p.b x) = y ∈ T ⇐⇒ x = (p.f y) ∈ T)
BY
{ Auto }

1
1. T : Type
2. p : Perm(T)
3. x : T
4. y : T
5. (p.b x) = y ∈ T
⊢ x = (p.f y) ∈ T

2
1. T : Type
2. p : Perm(T)
3. x : T
4. y : T
5. x = (p.f y) ∈ T
⊢ (p.b x) = y ∈ T

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}p:Perm(T).  \mforall{}x,y:T.    ((p.b  x)  =  y  \mLeftarrow{}{}\mRightarrow{}  x  =  (p.f  y))


By

---

Latex:
Auto

---

Home Index