Level: Lib Thy Top: 1
Hypotheses:None
Conclusion:
A,B:
. f:A 
B. R:B B 
.
(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)
Applied Tactic: (Reduce 0 THENM GenExRepD ...a)
Generated subgoals:1. (f a) R (f a)2. (f b) R (f a)
3. (f a) R (f c)