mb
label
Sections
GenAutomata
Doc
Rank
Theorem
Name
2
Thm*
x:Label, ls:Label List. x
ls
(x
ls)
[assert_lbls_member]
cites
1
Thm*
l1,l2:Label. l1 =
l2
l1 = l2
[assert_eq_label]
mb
label
Sections
GenAutomata
Doc
x:Label, ls:Label List. x 
ls 
(x ls)l1,l2:Label. l1 =
l2 
l1 = l2x:Label, ls:Label List. x ls (x ls)l1,l2:Label. l1 = l2 l1 = l2