mb automata 3 Sections GenAutomata Doc

Def rel_eq(a;b) == eq_relname(a.name;b.name)termlist_eq(a.args;b.args)

is mentioned by

Thm* a,b:rel(). rel_eq(a;b) a = b[assert_rel_eq]

Try larger context: GenAutomata

mb automata 3 Sections GenAutomata Doc