Thms
relation
autom
Sections
AutomataTheory
Doc
preima_of_rel
Def
R_f(x,y) == (f(x)) R (f(y))
Thm*
A,B:Type, f:(A
B), R:(B
B
Prop). R_f
A
A
Prop
About:
A,B:Type, f:(A
B), R:(BBProp). R_f 
AAProp
