(6steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

At: remove msgs disjoint 1 1
1. A: Type
2. msg: AA
3. L1: A List
4. L2: A List
5. a,b:A. (a L1) (b L2) msg(a,b)

(xL1.(a.reduce(b,y. msg(a,b)y;true;L2))(x))
By:
Unfolds [`l_all`;`so_apply`] 0
THEN
Reduce 0
THEN
RWO "l_all_reduce < " 0
Generated subgoal:

1 x:A. (x L1) (bL2.msg(x,b))

About:
listboolbtrueassertlambdaapplyfunctionuniverseimpliesall

(6steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc