(11steps)
PrintForm
Definitions
Lemmas
mb
hybrid
Sections
GenAutomata
Doc
At:
remove
msgs
nil
1
1
1
1
1
1.
A:
Type
2.
msg:
A
A
3.
L1:
A List
4.
L2:
A List
5.
x:A. (x
L1)
(x
L2)
6.
Refl(A)(msg(_1,_2))
7.
x:
A
8.
(x
L1)
(
b:A. (b
L2)
msg(x,b))
By:
Analyze 0
Generated subgoal:
1
9.
b:A. (b
L2)
msg(x,b)
False
About:
(11steps)
PrintForm
Definitions
Lemmas
mb
hybrid
Sections
GenAutomata
Doc
b:A. (b 
L2) 
msg(x,b)
False
A
x:A. (x L1) (x L2) L1) (b:A. (b L2) msg(x,b))b:A. (b L2) msg(x,b) False
