At:
map before
1
1
1.
T: Type
2.
T': Type
3.
f: T
T'
4.
x: T
5.
y: T
6.
s: T List
7.
f1: 
2||s||
8.
j:2. [x; y][j] = s[(f1(j))]
9.
j: 2
10.
[x; y][j] = s[(f1(j))]
[(f(x)); (f(y))][j] = f([x; y][j])
By:
CaseNat 0 `j'
THEN
Reduce 0
THEN
CaseNat 1 `j'
THEN
Reduce 0
Generated subgoals:
None
About:
