Step * 1 of Lemma perm_f_inj


1. Type
2. Perm(T)
3. T
4. T
5. (p.f x) (p.f y) ∈ T
⊢ y ∈ T
BY
(AddProperties THENA Auto) }

1
1. Type
2. Perm(T)
3. InvFuns(T;T;p.f;p.b)
4. T
5. T
6. (p.f x) (p.f y) ∈ T
⊢ y ∈ T


Latex:


Latex:

1.  T  :  Type
2.  p  :  Perm(T)
3.  x  :  T
4.  y  :  T
5.  (p.f  x)  =  (p.f  y)
\mvdash{}  x  =  y


By


Latex:
(AddProperties  2  THENA  Auto)




Home Index