PrintForm Definitions relation autom Sections AutomataTheory Doc

At: quotient 1 1 corr 1 1 1 3 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. F: (x,y:A//(x R_f y))(x,y:B//(x R y))
11. F = (x.f(x))
12. x1: B
13. x2: B
14. x1 R x2

(g(x1)) R_f (g(x2))
By:
Unfold `preima_of_rel` 0
THEN
Reduce 0
THEN
RWH add_composeC 0
Generated subgoal:

1 ((f o g)(x1)) R ((f o g)(x2))

About:
applyuniversefunctionpropquotientequallambda