mb automata 1 Sections GenAutomata Doc

TheoremName
Thm* s1,s2:SimpleType. st_eq(s1;s2) s1 = s2[assert_st_eq]
cites
Thm* l:Pattern. l = l[eq_lbl_reflexive]

mb automata 1 Sections GenAutomata Doc