At:
list-decomp-last
2
1
1
1
1.
T: Type
2.
s: T List
3.
u: T
4.
u1: T
5.
v1: T List
6.
0 < ||[u1 / v1]||+1
7.
0 < ||v1||+1+1-1
8.
[u1 / v1] ~ (firstn(||[u1 / v1]||-1;[u1 / v1]) @ [[u1 / v1][(||[u1 / v1]||-1)]])
firstn(||v1||+1+1-1-1;[u1 / v1]) ~ firstn(||[u1 / v1]||-1;[u1 / v1])
By:
Analyze
THEN
Reduce 0
Generated subgoals:
None
About:
