PrintForm Definitions relation autom Sections AutomataTheory Doc

At: quotient 1 1 corr 1 1 1 1 1 1
1. A: Type
2. B: Type
3. f: AB
4. R: BBProp
5. Bij(A; B; f)
6. EquivRel x,y:B. x R y
7. EquivRel x,y:A. x R_f y
8. g: BA
9. InvFuns(A; B; f; g)
10. x1: A
11. x2: A
12. x1 R_f x2

f(x1) = f(x2) x,y:B//(x R y)
By:
Unfold `preima_of_rel` -1
THEN
Reduce -1
Generated subgoal:

112. (f(x1)) R (f(x2))
f(x1) = f(x2) x,y:B//(x R y)

About:
equalquotientapplyuniversefunctionprop