At: remove msgs nil 1 1 1 1 1 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. x: A
8. (x L1)
9. b:A. (b L2) 
msg(x,b)
10. msg(x,x)
False
By:
RW assert_pushdownC -1
THEN
Analyze -1
Generated subgoal:| 1 | msg(x,x) |
About:
