a,z:
, n:
, s:({a...z}
{1...n}Peg), n':.
Thm* n
n'
Thm*
Thm* (
h:({n+1...n'}Peg), i:{1...n'}.
Thm* (i
n (x:{a...z}. (s(?) {to n} 
h {to n'})(x,i) = s(x,i)))n:, f:({1...n}Peg), n':.
Thm* n
n'
Thm*
Thm* (
f':({n+1...n'}Peg), i:{1...n'}.
Thm* (i
n (f {to n} f' {to n'})(i) = f(i))