Level: Lib Thy Top:
Hypotheses:None
Conclusion:
A,B:
. f:A 
B. R:B B 
. EquivRel(B;x,y.x R y) 
EquivRel(A;x,y.x R_f y)
Applied Tactic: (Unfolds ``equiv_rel preima_of_rel`` 0 THENM Unfolds ``refl sym trans`` 0 ...a)
Generated subgoals:1. 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)