mb
automata
1
Sections
GenAutomata
Doc
Theorem
Name
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