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. Type
2. Perm(T)
3. T
4. T
5. (p.f x) (p.f y) ∈ T
⊢ 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