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

At: remove msgs nil 1
1. A: Type
2. msg: AA
3. L1: A List
4. L2: A List
5. x:A. (x L1) (x L2)
6. Refl(A)(msg(_1,_2))

filter(a.reduce(b,y. msg(a,b)y;true;L2);L1) = nil
By: Inst Thm* P:(T), L:T List. (xL.P(x)) (filter(P;L) ~ nil) [A;a.reduce(b,y. msg(a,b)y;true;L2);L1]
Generated subgoals:

1 (xL1.(a.reduce(b,y. msg(a,b)y;true;L2))(x))
27. filter(a.reduce(b,y. msg(a,b)y;true;L2);L1) ~ nil
filter(a.reduce(b,y. msg(a,b)y;true;L2);L1) = nil

About:
listnilboolbtrueassertlambdafunctionuniverseequalimpliesall

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