PrintForm Definitions relation autom Sections AutomataTheory Doc

At: quotient 1 1 corr 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)

F:((x,y:A//(x R_f y))(x,y:B//(x R y))). Bij(x,y:A//(x R_f y); x,y:B//(x R y); F)
By:
Let (F = (x.f(x)))
THEN
Let (G = g)
Generated subgoals:

1 (x.f(x)) (x,y:A//(x R_f y))(x,y:B//(x R y))
2 (x,y:A//(x R_f y))(x,y:B//(x R y)) Type{[1 | i 0]}
310. F: (x,y:A//(x R_f y))(x,y:B//(x R y))
11. F = (x.f(x))
g (x,y:B//(x R y))(x,y:A//(x R_f y))
410. F: (x,y:A//(x R_f y))(x,y:B//(x R y))
11. F = (x.f(x))
(x,y:B//(x R y))(x,y:A//(x R_f y)) Type{[1 | i 0]}
510. F: (x,y:A//(x R_f y))(x,y:B//(x R y))
11. F = (x.f(x))
12. G: (x,y:B//(x R y))(x,y:A//(x R_f y))
13. G = g (x,y:B//(x R y))(x,y:A//(x R_f y))
F:((x,y:A//(x R_f y))(x,y:B//(x R y))). Bij(x,y:A//(x R_f y); x,y:B//(x R y); F)

About:
existsfunctionquotientequallambda
applyuniversepropmember