PrintForm relation autom Sections AutomataTheory Doc

At: preima of equiv rel 1

A,B:Type, f:(AB), R:(BBProp). (a:B. a R a) & (a,b:B. (a R b) (b R a)) & (a,b,c:B. (a R b) (b R c) (a R c)) (a:A. a (x,y. (f(x)) R (f(y))) a) & (a,b:A. (a (x,y. (f(x)) R (f(y))) b) (b (x,y. (f(x)) R (f(y))) a)) & (a,b,c:A. (a (x,y. (f(x)) R (f(y))) b) (b (x,y. (f(x)) R (f(y))) c) (a (x,y. (f(x)) R (f(y))) c))
By:
Reduce 0
THEN
GenExRepD
Generated subgoals:

11. A: Type
2. B: Type
3. f: AB
4. R: BBProp
5. a:B. a R a
6. a,b:B. (a R b) (b R a)
7. a,b,c:B. (a R b) (b R c) (a R c)
8. a: A
(f(a)) R (f(a))
21. A: Type
2. B: Type
3. f: AB
4. R: BBProp
5. a:B. a R a
6. a,b:B. (a R b) (b R a)
7. a,b,c:B. (a R b) (b R c) (a R c)
8. a: A
9. b: A
10. (f(a)) R (f(b))
(f(b)) R (f(a))
31. A: Type
2. B: Type
3. f: AB
4. R: BBProp
5. a:B. a R a
6. a,b:B. (a R b) (b R a)
7. a,b,c:B. (a R b) (b R c) (a R c)
8. a: A
9. b: A
10. c: A
11. (f(a)) R (f(b))
12. (f(b)) R (f(c))
(f(a)) R (f(c))

About:
alluniversefunctionpropimpliesandlambdaapply