---

Step * of Lemma perm_f_inj

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

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index