A modeloid, a certain equivalence relation with an operation inspired by Ehrenfeucht-Fraïssé games, formulated by Miroslav Benda is generalized first to an inverse semigroup and then to an inverse category. It is shown that a categorical modeloid on the category of a finite vocabulary can be used to plan an Ehrenfeucht-Fraïssé game. On the way the Wagner-Preston representation theorem and the Ehrenfeucht-Fraïssé theorem are proven. The whole work is supported by using computer-based theorem proving.