PrintForm Definitions relation autom Sections AutomataTheory Doc

At: preima of equiv rel

A,B:Type, f:(AB), R:(BBProp). (EquivRel x,y:B. x R y) (EquivRel x,y:A. x R_f y)
By:
Unfolds [`equiv_rel`;`preima_of_rel`] 0
THEN
Unfolds [`refl`;`sym`;`trans`] 0
Generated subgoal:

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))

About:
alluniversefunctionpropimpliesandlambdaapply