(6steps)
PrintForm
Definitions
Lemmas
mb
hybrid
Sections
GenAutomata
Doc
At:
remove
msgs
disjoint
1
1
1
1.
A:
Type
2.
msg:
A
A
3.
L1:
A List
4.
L2:
A List
5.
a,b:A. (a
L1)
(b
L2)
msg(a,b)
x:A. (x
L1)
(
b
L2.
msg(x,b))
By:
Unfold `l_all` 0
Generated subgoal:
1
6.
x:
A
7.
(x
L1)
8.
b:
A
9.
(b
L2)
msg(x,b)
About:
(6steps)
PrintForm
Definitions
Lemmas
mb
hybrid
Sections
GenAutomata
Doc
L1) L2)
msg(x,b)
A
a,b:A. (a L1) 
(b L2) msg(a,b) x:A. (x L1) (bL2.msg(x,b)) L1) L2) msg(x,b)
