PrintForm Definitions relation autom Sections AutomataTheory Doc

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

(x.f(x)) (x,y:A//(x R_f y))(x,y:B//(x R y))
By: EqToMemberEq (i.EqCDAux `strong`) 0
Generated subgoals:

110. x: x,y:A//(x R_f y)
f(x) x,y:B//(x R y)
2 x,y:A//(x R_f y) Type

About:
memberfunctionquotientlambdaapplyuniverseprop