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

At: remove msgs nil

A:Type, msg:(AA), L1,L2:A List. (x:A. (x L1) (x L2)) Refl(A)(msg(_1,_2)) (L1 -msg(a,b) L2) = nil
By:
Auto
THEN
Unfold `remove_msgs` 0
Generated subgoal:

11. 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

About:
listnilboolbtrueassertlambdafunctionuniverseequalimpliesall

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