msg:(A
A
), L1,L2:A List.
(a,b:A. (a 
L1) 
(b L2) 
msg(a,b)) (L1 -msg(a,b) L2) = L1msg:(AA), L1,L2:A List.
(x:A. (x L1) (x L2)) Refl(A)(msg(_1,_2)) (L1 -msg(a,b) L2) = nil l) == 
i:
. i < ||l|| & x = l[i] T
is mentioned by
|
Thm* msg:(AA), L1,L2:A List.
(a,b:A. (a L1) (b L2) msg(a,b)) (L1 -msg(a,b) L2) = L1 | [remove_msgs_disjoint] |
|
Thm* msg:(AA), L1,L2:A List.
(x:A. (x L1) (x L2)) Refl(A)(msg(_1,_2)) (L1 -msg(a,b) L2) = nil | [remove_msgs_nil] |
In prior sections: mb list 1 mb label mb list 2 mb structures mb automata 1
Try larger context: GenAutomata