At: remove msgs nil 1 1 1 1 1 1
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)
False
By: InstHyp [x] -1
Generated subgoals:| 1 | (x L2) |
| 2 | 10. msg(x,x)
False |
About:
