At: preima of equiv rel 1 3
1. A: Type
2. B: Type
3. f: A
B
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))
By: FwdThru 7 [11;12]
Generated subgoals:None
About:
