PrintForm Definitions relation autom Sections AutomataTheory Doc

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

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: Inst Thm* f:(AB), R:(BBProp). (EquivRel x,y:B. x R y) (EquivRel x,y:A. x R_f y) [A;B;f;R]
Generated subgoal:

17. EquivRel 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:
existsfunctionquotientuniverseprop