(5steps)
PrintForm
Definitions
Lemmas
mb
label
Sections
GenAutomata
Doc
At:
assert
lbls
member
2
1
1.
x:
Label
2.
ls:
Label List
3.
u:
Label
4.
v:
Label List
5.
x
v
(x
v)
6.
x
v
(x
v)
7.
x =
u
x = u
By:
FwdThru
Thm*
l1,l2:Label. l1 =
l2
l1 = l2 [-1]
Generated subgoals:
None
About:
(5steps)
PrintForm
Definitions
Lemmas
mb
label
Sections
GenAutomata
Doc
v 
(x v) v 
(x v)
u
x = u
l1,l2:Label. l1 = l2 l1 = l2
[-1]
