At: remove msgs nil 1 2
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. 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
By: HypSubst -1 0
Generated subgoals:None
About: